ComputingComputer ScienceFormal MethodsLogicTheory Of ComputationDeductive ReasoningDeductive SystemsPredicate LogicProof AssistantsProof TheoryTheorem ProvingFormal Proof SystemsProof Systems
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.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">></ETX>