Automated Theorem Proving and Its Prospects [Book Review]

PSYCHE: An Interdisciplinary Journal of Research On Consciousness 2 (1995)
  Copy   BIBTEX

Abstract

REVIEW OF: Automated Development of Fundamental Mathematical Theories by Art Quaife. (1992: Kluwer Academic Publishers) 271pp. Using the theorem prover OTTER Art Quaife has proved four hundred theorems of von Neumann-Bernays-Gödel set theory; twelve hundred theorems and definitions of elementary number theory; dozens of Euclidean geometry theorems; and Gödel's incompleteness theorems. It is an impressive achievement. To gauge its significance and to see what prospects it offers this review looks closely at the book and the proofs it presents.

Categories

Keywords

Reprint years

Links

PhilArchive

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Automated Theorem-proving in Non-classical Logics.Paul B. Thistlewaite, Michael A. McRobbie & Robert K. Meyer - 1988 - Pitman Publishing.
Thephilosophyofautomatedtheoremproving.Francis Jeffry Pelletier - unknown
First-Order Logic and Automated Theorem Proving.Melvin Fitting - 1998 - Studia Logica 61 (2):300-302.
Human-oriented and machine-oriented reasoning: Remarks on some problems in the history of Automated Theorem Proving. [REVIEW]Furio Di Paola - 1988 - AI and Society 2 (2):121-131.
Isabelle: A Generic Theorem Prover.Lawrence C. Paulson - 1994 - Springer Verlag.
Automated theorem proving for łukasiewicz logics.Gordon Beavers - 1993 - Studia Logica 52 (2):183 - 195.
Automated Deduction - CADE-16: 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings.Harald Ganzinger - 1999 - Springer Verlag.
Automated Deduction - Cade-18: 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002 Proceedings.Andrei Voronkov - 2002 - Springer Verlag.
Automated Deduction - Cade-17: 17th International Conference on Automated Deduction Pittsburgh, Pa, Usa, June 17-20, 2000 Proceedings.David McAllester - 2000 - Springer Verlag.
Automated Deduction, CADE-11: 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992 : Proceedings.Deepak Kapur - 1992 - Springer.
Automated Deduction - CADE-15: 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings.Claude Kirchner & Helene Kirchner - 1998 - Springer Verlag.
Automated Deduction - Cade-13: 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30 - August 3, 1996. Proceedings.Michael A. McRobbie & J. K. Slaney - 1996 - Springer Verlag.
Automated Deduction - CADE-14: 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13 - 17, 1997, Proceedings.William McCune - 1997 - Lecture Notes in Artificial Intelligence.
Automated Deduction - CADE-19: 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings.Franz Baader - 2003 - Springer Verlag.
Automated Deduction, Cade-12.: 12th International Conference on Automated Deduction, Nancy, France, June 26 - July 1, 1994. Proceedings.Alan Bundy - 1994 - Springer Verlag.

Analytics

Added to PP
2015-02-05

Downloads
175 (#108,920)

6 months
59 (#74,980)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Desmond Sander
University of Tasmania

Citations of this work

No citations found.

Add more citations

References found in this work

Science and method.Henri Poincaré - 1914 - New York]: Dover Publications. Edited by Francis Maitland.
Science and method.Henri Poincaré - 1914 - Mineola, N.Y.: Dover Publications. Edited by Francis Maitland.
A Machine-Oriented Logic based on the Resolution Principle.J. A. Robinson - 1966 - Journal of Symbolic Logic 31 (3):515-516.
An examination of the geometry theorem machine.P. C. Gilmore - 1970 - Artificial Intelligence 1 (3-4):171-187.

Add more references