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.


Inference Rule Propositional Logic Function Symbol Predicate Logic Conjunctive Normal Form 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. [Bib82]
    W. Bibel. Automated Theorem Proving. Vieweg, Wiesbaden, 1982. MATHGoogle Scholar
  2. [CAD]
    CADE: Conference on Automated Deduction. www.cadeconference.org.
  3. [CL73]
    C. L. Chang and R. C. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, Orlando, 1973. MATHGoogle Scholar
  4. [Ede91]
    E. Eder. Relative Complexities of First Order Calculi. Vieweg, Wiesbaden, 1991. Google Scholar
  5. [Fit96]
    M. Fitting. First-Order Logic and Automated Theorem Proving. Springer, Berlin, 1996. MATHGoogle Scholar
  6. [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
  7. [Göd31a]
    K. Gödel. Diskussion zur Grundlegung der Mathematik, Erkenntnis 2. Monatshefte Math. Phys., 32(1):147–148, 1931. Google Scholar
  8. [Kal01]
    J. A. Kalman. Automated Reasoning with OTTER. Rinton, Paramus, 2001. www-unix.mcs.anl.gov/AR/otter/index.html. MATHGoogle Scholar
  9. [Lov78]
    D. W. Loveland. Automated Theorem Proving: A Logical Basis. North-Holland, Amsterdam, 1978. MATHGoogle Scholar
  10. [LSBB92]
    R. Letz, J. Schumann, S. Bayerl, and W. Bibel. SETHEO: a high-performance theorem prover. J. Autom. Reason., 8(2):183–212, 1992. www4.informatik.tu-muenchen.de/~letz/setheo. CrossRefMATHMathSciNetGoogle Scholar
  11. [McC]
    W. McCune. Automated deduction systems and groups. www-unix.mcs.anl.gov/AR/others.html. See also www-formal.stanford.edu/clt/ARS/systems.html.
  12. [New00]
    M. Newborn. Automated Theorem Proving: Theory and Practice. Springer, Berlin, 2000. Google Scholar
  13. [NPW02]
    T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL—A Proof Assistant for Higher-Order Logic. LNCS, volume 2283. Springer, Berlin, 2002. www.cl.cam.ac.uk/Research/HVG/Isabelle. MATHGoogle Scholar
  14. [Sch01]
    J. Schumann. Automated Theorem Proving in Software Engineering. Springer, Berlin, 2001. Google Scholar
  15. [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
  16. [SET09]
    T. Segaran, C. Evans, and J. Taylor. Programming the Semantic Web. O’Reilly, Cambridge, 2009. Google Scholar
  17. [SS06]
    G. Sutcliffe and C. Suttner. The state of CASC. AI Commun., 19(1):35–48, 2006. CASC-Homepage: www.cs.miami.edu/~tptp/CASC. MATHMathSciNetGoogle Scholar
  18. [vA06]
    L. v. Ahn. Games with a purpose. IEEE Comput. Mag., 96–98, June 2006. http://www.cs.cmu.edu/~biglou/ieee-gwap.pdf.

Copyright information

© Springer-Verlag London Limited 2011

Authors and Affiliations

  1. 1.FB Elektrotechnik und InformatikHochschule Ravensburg-Weingarten, University of Applied SciencesWeingartenGermany

Personalised recommendations