First-order Predicate Logic
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.
KeywordsInference Rule Propositional Logic Function Symbol Predicate Logic Conjunctive Normal Form
- [CAD]CADE: Conference on Automated Deduction. www.cadeconference.org.
- [Ede91]E. Eder. Relative Complexities of First Order Calculi. Vieweg, Wiesbaden, 1991. Google Scholar
- [FS97]B. Fischer and J. Schumann. Setheo goes software engineering: application of atp to software reuse. In Conference on Automated Deduction (CADE-14). LNCS, volume 1249, pages 65–68. Springer, Berlin, 1997. http://ase.arc.nasa.gov/people/schumann/publications/papers/cade97-reuse.html. Google Scholar
- [Göd31a]K. Gödel. Diskussion zur Grundlegung der Mathematik, Erkenntnis 2. Monatshefte Math. Phys., 32(1):147–148, 1931. Google Scholar
- [New00]M. Newborn. Automated Theorem Proving: Theory and Practice. Springer, Berlin, 2000. Google Scholar
- [Sch01]J. Schumann. Automated Theorem Proving in Software Engineering. Springer, Berlin, 2001. Google Scholar
- [Sch02]S. Schulz. E—a brainiac theorem prover. J. AI Commun., 15(2/3):111–126, 2002. www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html. MATHGoogle Scholar
- [SET09]T. Segaran, C. Evans, and J. Taylor. Programming the Semantic Web. O’Reilly, Cambridge, 2009. Google Scholar
- [vA06]L. v. Ahn. Games with a purpose. IEEE Comput. Mag., 96–98, June 2006. http://www.cs.cmu.edu/~biglou/ieee-gwap.pdf.