Until the end of the 20th century many logicians believed that theorem provers for first-order logic will be the major component of intelligent agents. Almost all successful modern AI applications however use different formalisms. This is due to some severe problems with first-order logic that we will explain in this chapter.


Bayesian Network Predicate Logic Default Logic Situation Calculus Automate Prover 
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. [ESS89]
    W. Ertel, J. Schumann, and Ch. Suttner. Learning heuristics for a theorem prover using back propagation. In J. Retti and K. Leidlmair, editors, 5. Österreichische Artificial-Intelligence-Tagung. Informatik-Fachberichte, volume 208, pages 87–95. Springer, Berlin, 1989. Google Scholar
  2. [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
  3. [PS09]
    G. Pólya and S. Sloan. How to Solve It: A New Aspect of Mathematical Method. Ishi, Mountain View, 2009. Google Scholar
  4. [SB04]
    J. Siekmann and Ch. Benzmüller. Omega: computer supported mathematics. In KI 2004: Advances in Artificial Intelligence. LNAI, volume 3238, pages 3–28. Springer, Berlin, 2004. www.ags.uni-sb.de/~omega. Google Scholar
  5. [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
  6. [SE90]
    Ch. Suttner and W. Ertel. Automatic acquisition of search guiding heuristics. In 10th Int. Conf. on Automated Deduction. LNAI, volume 449, pages 470–484. Springer, Berlin, 1990. Google Scholar
  7. [Wie]
    U. Wiedemann. PhilLex, Lexikon der Philosophie. www.phillex.de/paradoxa.htm.

Copyright information

© Springer-Verlag London Limited 2011

Authors and Affiliations

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

Personalised recommendations