Abstract
We survey research in the automation of deductive inference, from its beginnings in the early history of computing to the present day. We identify and describe the major areas of research interest and their applications. The area is characterised by its wide variety of proof methods, forms of automated deduction and applications.
I would like to thank Richard Boulton, Michael Fisher, Ian Frank, Predrag Janičić, Andrew Ireland and Helen Lowe for feedback on an earlier version of this survey. I would also like to thank Carole Douglas for help in its preparation.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Rajeev Alur and Thomas A. Henzinger, editors. Proceedings of the 1996 Conference on Computer-Aided Verification, number 1102 in LNCS, New Brunswick, New Jersey, U. S. A., 1996. Springer-Verlag.
P. B. Andrews, M. Bishop, I. Sunil, D. Nesmith, F. Pfenning, and H. Xi. TPS: A theorem proving system for classical type theory. Journal of Automated Reasoning, 16(3):321–353, 1996.
L. Augustsson, T. Coquand, and B. Nordström. A short description of another logical framework. In Proceedings of the First Workshop on Logical Frameworks, Antibes, pages 39–42, 1990.
L. Bachmair and H. Ganzinger. On restrictions of ordered paramodulation with simplification. In M. E. Stickel, editor, Proc. 10th Int. Conf. on Automated Deduction, Kaiserslautern, volume 449, pages 427–441. Springer-Verlag, 1990.
L. Bachmair and H. Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217–247, 1994. Revised version of Research Report MPI-I-91-208, 1991.
R. Backhouse, editor. 2nd International Workshop on User Interfaces for Theorem Provers, 1998.
H. P. Barendregt. The Lambda Calculus. Elsevier, 1985.
David Basin and Toby Walsh. A calculus for and termination of rippling. Journal of Automated Reasoning, 16(1–2):147–180, 1996.
S. Biundo, B. Hummel, D. Hutter, and C. Walther. The Karlsruhe induction theorem proving system. In Joerg Siekmann, editor, 8th International Conference on Automated Deduction, pages 672–674. Springer-Verlag, 1986. Springer Lecture Notes in Computer Science No. 230.
W. W. Bledsoe. The Sup-Inf method in Presburger arithmetic. Memo ATP-18, Department of Mathematics, University of Texas at Austin, USA, Dec 1974.
E. Borger and D. Rosenzweig. A mathematical definition of full Prolog. Science of Computer Programming, 24:249–286, 1994.
A. Bouhoula, E. Kounalis, and M. Rusinowitch. SPIKE: an automatic theorem prover. In Proceedings of LPAR’ 92, number 624 in LNAI. Springer-Verlag, July 1992.
R. S. Boyer and J S. Moore. A Computational Logic Handbook. Academic Press, 1988. Perspectives in Computing, Vol 23.
R. Brachman, H. Levesque, and Reiter. R, editors. Artificial Intelligence, volume 49. Elsevier, 1991.
R. E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293–318, September 1992.
A. Bundy, F. van Harmelen, C. Horn, and A. Smaill. The Oyster-Clam system. In M. E. Stickel, editor, 10th International Conference on Automated Deduction, pages 647–648. Springer-Verlag, 1990. Lecture Notes in Artificial Intelligence No. 449. Also available from Edinburgh as DAI Research Paper 507.
A. Bundy, A. Stevens, F. van Harmelen, A. Ireland, and A. Smaill. Rippling: A heuristic for guiding inductive proofs. Artificial Intelligence, 62:185–253, 1993. Also available from Edinburgh as DAI Research Paper No. 567.
Alan Bundy. A science of reasoning. In J.-L. Lassez and G. Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson, pages 178–198. MIT Press, 1991. Also available from Edinburgh as DAI Research Paper 445.
Alan Bundy, editor. 12th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, Vol. 814, Nancy, Prance, 1994. Springer-Verlag.
Stefano Ceri, Georg Gottlob, and Leitzia Tanca. Logic Programming and Databases. Surveys in Computer Science. Springer-Verlag, Berlin, 1990.
B.F. Chellas. Modal Logic: An Introduction. Cambridge University Press, 1980.
S-C Chou. Mechanical Geometry Theorem Proving. Reidel Pub. Co., Dordrecht, 1988.
W. F. Clocksin and C. S. Mellish. Programming in Prolog. Springer Verlag, 1981.
R. L. Constable, S. F. Allen, H. M. Bromley, et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, 1986.
D. C. Cooper. Theorem proving in arithmetic without multiplication. In B. Meltzer and D. Michie, editors, Machine Intelligence 7, pages 91–99. Edinburgh University Press, 1972.
M. Davis and H. Putnam. A computing procedure for quantification theory. J. Association for Computing Machinery, 7:201–215, 1960.
Nachum Dershowitz. Orderings for term rewriting systems. Journal of Theoretical Computer Science, 17(3):279–301, 1982.
G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Paulin, and B. Werner. The Coq proof assistant user’s guide, version 5.6. Technical Report 134, INRIA, 1991.
M.J. Fay. First-order unification in an equational theory. In Procs. of the Fourth Workshop on Automated Deduction, pages 161–167. Academic Press, 1979.
R. E. Fikes, and N. J. Nilsson. STRIPS: A new approach to the application of theorem proving to problem solving. Artificial Intelligence, 2:189–208, 1971.
H. Gelernter. Empirical explorations of the geometry theorem-proving machine. In E. Feigenbaum and J. Feldman, editors, Computers and Thought, pages 153–163. McGraw Hill, 1963.
H. Gelernter. Realization of a geometry theorem-proving machine. In E. Feigenbaum and J. Feldman, editors, Computers and Thought, pages 134–152. McGraw Hill, 1963.
P. C. Gilmore. A proof method for quantificational theory. IBM J Res. Dev., 4:28–35, 1960.
J.-Y. Girard, Y. Lafont, and L. Regnier, editors. Advances in Linear Logic. Number 222 in London Mathematical Society Lecture Note Series. Cambridge University Press, Cambridge, 1995.
K. Gödel. Über formal unentscheidbare sätze der principia mathematica und verwandter systeme i. Monatsh. Math. Phys., 38:173–198, 1931. English translation in [42].
M. J. Gordon, A. J. Milner, and C. P. Wadsworth. Edinburgh LCF-A mechanised logic of computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.
M. J. Gordon. HOL: A proof generating system for higher-order logic. In G. Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis. Kluwer, 1988.
Cordell Green. Application of theorem proving to problem solving. In Proceedings of the 1st International Joint Conference on Artificial Intelligence, pages 219–239, Washington, D. C., U. S. A., 1969.
J. Y. Halpern and Y. Moses. A guide to completeness and complexity for modal logics of knowledge and belief. Artificial Intelligence, 54:319–379, 1992.
M. Hanus. The integration of functions into logic programming: from theory to practice. J. Logic Programming, 19 & 20:583–628, 1994.
P Hayes. In defence of logic. In Proceedings of IJCAI-77, pages 559–565. International Joint Conference on Artificial Intelligence, 1977.
J van Heijenoort. From Frege to Gödel: a source book in Mathematical Logic, 1879–1931. Harvard University Press, Cambridge, Mass, 1967.
J. Herbrand. Researches in the theory of demonstration. In J van Heijenoort, editor, From Frege to Goedel: a source book in Mathematical Logic, 1879–1931, pages 525–581. Harvard University Press, Cambridge, Mass, 1930.
P. M. Hill and J. W. Lloyd. The Gödel Programming Language. MIT Press, 1994.
Louis Hodes. Solving problems by formula manipulation in logic and linear inequalities. In Proceedings of the 2nd International Joint Conference on Artificial Intelligence, pages 553–559, Imperial College, London, England, 1971. The British Computer Society.
G. Huet and D. C. Oppen. Equations and rewrite rules: A survey. In R. Book, editor, Formal languages: Perspectives and open problems. Academic Press, 1980. Presented at the conference on formal language theory, Santa Barbara, 1979. Available from SRI International as technical report CSL-111.
G. Huet and G. D. Plotkin. Logical Frameworks. CUP, 1991.
G. Huet. A unification algorithm for typed lambda calculus. Theoretical Computer Science, 1:27–57, 1975.
D. Hutter. Coloring terms to control equational reasoning. Journal of Automated Reasoning, 18(3):399–442, 1997.
A. Ireland and A. Bundy. Productive use of failure in inductive proof. Journal of Automated Reasoning, 16(1–2):79–111, 1996. Also available as DAI Research Paper No 716, Dept. of Artificial Intelligence, Edinburgh.
J. Jaffar and M. Maher. Constraint logic programming: A survey. Journal of Logic Programming, 19/20:503–581, 1994.
Jean-Pierre Jouannaud and Claude Kirchner. Solving equations in abstract algebras: A rule-based survey of unification. In Jean-Louis Lassez and Gordon Plotkin, editors, Computational Logic, chapter 8, pages 257–321. MIT Press, 1991.
D. Kapur and I. Wos, editors. Journal of Automated Reasoning, volume 21. Kluwer, 1998.
D. Kapur and H. Zhang. An overview of rewrite rule laboratory (RRL). J. of Computer Mathematics with Applications, 29(2):91–114, 1995.
D. Kapur, P. Narendran, and H. Zhang. Automating inductionless induction by test sets. Journal of Symbolic Computation, 11:83–111, 1991.
D. E. Knuth and P. B. Bendix. Simple word problems in universal algebra. In J. Leech, editor, Computational problems in abstract algebra, pages 263–297. Pergamon Press, 1970.
H. J. Komorowski. Partial evaluation as a means for inferencing data structures in an applicative language: A theory and implementation in the case of PROLOG. In Proceedings of the ninth conference on the Principles of Programming Languages (POPL), pages 225–267, Albuquerque, New Mexico, 1982. ACM.
R. Kowalski, F. Sadri, and P. Soper. Integrity checking in deductive databases. In Proc. 13th VLDB, Brighton, pages 61–69. Morgan Kaufmann, 1987.
R. Kowalski. Logic for Problem Solving. Artificial Intelligence Series. North Holland, 1979.
G. Kreisel. Mathematical logic. In T. Saaty, editor, Lectures on Modern Mathematics, volume 3, pages 95–195. J. Wiley & Sons, 1965.
D. W. Loveland. Automated theorem proving: A logical basis, volume 6 of Fundamental studies in Computer Science. North Holland, 1978.
H. Lowe and D. Duncan. XBarnacle: Making theorem provers more accessible. In William McCune, editor, 14th International Conference on Automated Deduction, pages 404–408. Springer-Verlag, 1997.
M. Lowry, A. Philpot, T. Pressburger, and I. Underwood. Amphion: Automatic programming for scientific subroutine libraries. In Proc. 8th Intl. Symp. on Methodologies for Intelligent Systems, Charlotte, North Carolina, October 1994.
Z. Luo and R. Pollack. Lego proof development system: User’s manual. Report ECS-LFCS-92-211, Department of Computer Science, University of Edinburgh, May 1992.
E.L. Lusk, W.W. McCune, and J. Slaney. Roo: A parallel theorem prover. In Deepak Kapur, editor, 11th International Conference on Automated Deduction, pages 731–734, Saratoga Springs, NY, USA, June 1992. Published as Springer Lecture Notes in Artificial Intelligence, No 607.
Z. Manna. et al Step: the Stanford temporal prover. Technical Report STAN-CS-TR;94-1518, Stanford University, 1994.
P. Martin-Lof. Notes on Constructive Mathematics. Almqvist and Wiksell, Stockholm, 1970.
J. McCarthy. Programs with common sense. In Mechanisation of Thought Processes (Proceedings of a symposium held at the National Physics Laboratory, London, Nov 1959), pages 77–84, London, 1959. HMSO.
W. McCune. Solution of the Robbins problem. J. Automated Reasoning, 19(3):263–276, 1997.
C. S. Mellish. Abstract interpretation of Prolog programs. In S. Abramsky and C. Hankin, editors, Abstract Interpretation of Declarative Languages, pages 181–197. Ellis Horwood, 1987.
D. Miller and G. Nadathur. An overview of λProlog. In R. Bowen, & K. Kowalski, editor, Proceedings of the Fifth International Logic Programming Conference/ Fifth Symposium on Logic Programming. MIT Press, 1988.
D. Miller. Unification of simply typed lambda-terms as logic programming. In P.K. Furukawa, editor, Proc. 1991 Joint Int. Conf. Logic Programming, pages 253–281. MIT Press, 1991.
S.H. Muggleton. Inductive logic programming. New Generation Computing, 8(4):295–318, 1991.
G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245–257, October 1979.
A. Newell, J. C. Shaw, and H. A. Simon. Empirical explorations with the Logic Theory Machine. In Proc. West. Joint Comp. Conf., pages 218–239, 1957. Reproduced in Computers and Thought (eds Feigenbaum and Feldman), McGraw Hill, New York, pp 109–133, 1963.
H.J. Ohlbach. Semantics based translation methods for modal logics. Journal of Logic and Computation, 1(5):691–746, 1991.
R. A. Overbeek and E. L. Lusk. Logic data structures and control architecture for implementation of theorem proving programs. In W. Bibel and R. Kowalski, editors, 5th International Conference on Automated Deduction. Springer Verlag, 1980. Lecture Notes in Computer Science No. 87.
S. Owen. Analogy for Automated Reasoning. Academic Press Ltd, 1990.
S. Owre, J. M. Rushby, and N. Shankar. PVS: An integrated approach to specification and verification. Tech report, SRI International, 1992.
L.C. Paulson. Natural deduction as higher order resolution. Journal of Logic Programming, 3:237–258, 1986.
L.C. Paulson. ML for the Working Programmer. Cambridge University Press, 1991.
J. Pearl. Probabilistic Reasoning in Intelligent Systems: Networks of Plausible Inference. Morgan Kaufmann, 1988.
F. Pfenning. Logic programming in the LF logical framework. In Logical Frame works, pages 149–182. Cambridge University Press, 1991.
G. Plotkin. A note on inductive generalization. In D Michie and B Meltzer, editors, Machine Intelligence 5, pages 153–164. Edinburgh University Press, 1969.
G. Plotkin. Building-in equational theories. In D Michie and B Meltzer, editors, Machine Intelligence 7, pages 73–90. Edinburgh University Press, 1972.
Mojżesz Presburger. Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In Sprawozdanie z I Kongresu metematyków slowiańskich, Warszawa 1929, pages 92–101, 395. Warsaw, 1930. Annotated English version also available [93].
U. S. Reddy. Term rewriting induction. In Proc. of Tenth International Conference on Automated Deduction. Springer-Verlag, 1990.
G. Robinson and L. Wos. Paramodulation and theorem-proving in first-order theories with equality. In D. Michie, editor, Machine Intelligence 4, pages 103–33. Edinburgh University Press, 1969.
J. A. Robinson. A machine oriented logic based on the resolution principle. J Assoc. Comput. Mach., 12:23–41, 1965.
R. E. Shostak. Deciding combinations of theories. Journal of the ACM, 31(1):1–12, January 1984. Also: Proceedings of the 6th International Conference on Auto mated Deduction, volume 138 of Lecture Notes in Computer Science, pages 209–222. Springer-Verlag, June 1982.
J. R. Slagle. A heuristic program that solves symbolic integration problems in freshman calculus. In E. A. Feigenbaum and J. Feldman, editors, Computers and Thought, pages 191–203. McGraw Hill, 1963.
J. Slaney. The crisis in finite mathematics: automated reasoning as cause and cure. In Bundy [19], pages 1–13.
Ryan Stansifer. Presburger’s article on integer arithmetic: Remarks and translation. Technical Report TR 84-639, Department of Computer Science, Cornell University, September 1984.
M. E. Stickel. A Prolog technology theorem prover. New Generation Computing, 2(4):371–83, 1984.
G.J. Sussman, T. Winograd, and E. Charniak. Micro-planner reference manual. Technical Report 203a, MIT AI Lab, 1971.
G. Sutcliffe, C. Suttner, and T. Yemenis. The TPTP problem library. In Bundy [19], pages 252–266.
C. Suttner and G. Sutcliffe. The CADE-14 ATP system competition. Journal of Automated Reasoning, 21(1):99–134, 1998.
L. A. Wallen. Automated Proof Search in Non-Classical Logics. MIT Press, London, 1990.
T. Walsh, A. Nunes, and Alan Bundy. The use of proof plans to sum series. In D. Kapur, editor, 11th International Conference on Automated Deduction, pages 325–339. Springer Verlag, 1992. Lecture Notes in Computer Science No. 607. Also available from Edinburgh as DAI Research Paper 563.
C. Walther. Combining induction axioms by machine. In Proceedings of IJCAI-93, pages 95–101. International Joint Conference on Artificial Intelligence, 1993.
C. Walther. Mathematical induction. In C. J. Hogger D. M. Gabbay and J. A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 12, pages 122–227. Oxford University Press, Oxford, 1994.
C. Walther. On proving termination of algorithms by machine. Artificial Intelligence, 71(1):101–157, 1994.
R. W. Weyhrauch. Prolegomena to a theory of mechanized formal reasoning. Artificial Intelligence, 13:133–170, 1980.
L. Wos, R. Overbeek, E. Lusk, and J. Boyle. Automated Reasoning: Introduction and Applications. Prentice-Hall, 1984.
L. Wos. Automated reasoning answers open questions. Notices of the AMS, 5(1):15–26, January 1993.
Wen-Tsün Wu. The Char-Set method and its applications to automated reasoning. In William McCune, editor, 14th International Conference on Automated Deduction, pages 1–4. Springer-Verlag, 1997.
Tetsuya Yoshida, Alan Bundy, Ian Green, Toby Walsh, and David Basin. Coloured rippling: An extension of a theorem proving heuristic. In A. G. Cohn, editor, In proceedings of ECAI-94, pages 85–89. John Wiley, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Bundy, A. (1999). A Survey of Automated Deduction. In: Wooldridge, M.J., Veloso, M. (eds) Artificial Intelligence Today. Lecture Notes in Computer Science(), vol 1600. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48317-9_6
Download citation
DOI: https://doi.org/10.1007/3-540-48317-9_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66428-4
Online ISBN: 978-3-540-48317-5
eBook Packages: Springer Book Archive