Swipe to navigate through the chapters of this book
In the 1930s Kurt Gödel Alonso Church, and Alan Turing laid important foundations for logic and, theoretical computer science. Of particular interest for AI are Gödel’s theorems. The completeness theorem states that first-order predicate logic is complete. This means that every true statement that can be formulated in predicate logic is provable using the rules of a formal calculus. Using programmable computers, on this basis, automatic theorem provers could later be constructed as implementations of formal calculi. We introduce the language of first-order predicate logic, develop the resolution calculus and show how automated theorem provers can be built and applied to prove relevant problems in every day reasoning and software engineering.
Please log in to get access to this content
To get access to this content you need the following product:
CADE is the annual “Conference on Automated Deduction” [CAD] and ATP stands for “Automated Theorem Prover”.
- First-order Predicate Logic
- Springer International Publishing
- Sequence number
- Chapter number
- Chapter 3