Title :
Proving unprovability
Author_Institution :
Dept. of Comput. Sci., Technion-Israel Inst. of Technol., Haifa, Israel
Abstract :
A formal proof system for unprovability in the predicate calculi is developed. This system is shown to be complete with respect to the logic of finite structures. It can be used to extend the ´negation by failure´ of Prolog, prevent infinite loops in a deductive data base or Prolog, or prove formulaes in nonmonotonic (default) logic.<>
Keywords :
logic programming; theorem proving; Prolog; deductive data base; formal proof system; logic of finite structures; nonmonotonic logic; predicate calculi; unprovability; Arithmetic; Artificial intelligence; Calculus; Computer science; Humans; Logic; Network address translation;
Conference_Titel :
Logic in Computer Science, 1988. LICS '88., Proceedings of the Third Annual Symposium on
Conference_Location :
Edinburgh, UK
Print_ISBN :
0-8186-0853-6
DOI :
10.1109/LICS.1988.5097
