The Basis of the Resolution Calculus

Abstract

Throughout the whole book we will focus on theorem proving in the context of first-order logic. First-order logic plays an important role in mathematical logic and computer science. First of all it is a rich language, by which algebraic theories, computational problems, and substantial knowledge representation in Artificial Intelligence can be expressed; due to its ability to represent undecidable problems (like the halting problem for Turing machines) first-order logic (or more precisely, the validity problem for first-order logic) is undecidable. On the other hand, the valid formulas of first-order logic can be obtained by logical calculi and thus are recursively enumerable. In this sense, first-order logic is mechanizable (we can find a proof for every valid sentence, but there is no decision procedure for validity).