The Automation of Proof by Mathematical Induction
Author:
- Alan BundyABAlan Bundy
- 1 January 2001
- book chapter
- Published by Elsevier
- p. 845-911
Abstract
No abstract availableThis publication has 14 references indexed in Scilit:
- An industrial strength theorem prover for a logic based on Common LispIEEE Transactions on Software Engineering, 1997
- Productive use of failure in inductive proofJournal of Automated Reasoning, 1996
- An overview of Rewrite Rule Laboratory (RRL)Computers & Mathematics with Applications, 1995
- On proving the termination of algorithms by machineArtificial Intelligence, 1994
- Rippling: A heuristic for guiding inductive proofsArtificial Intelligence, 1993
- Symbolic Boolean manipulation with ordered binary-decision diagramsACM Computing Surveys, 1992
- Deciding Combinations of TheoriesJournal of the ACM, 1984
- Accessible Independence Results for Peano ArithmeticBulletin of the London Mathematical Society, 1982
- Fast Decision Procedures Based on Congruence ClosureJournal of the ACM, 1980
- A synthesis of several sorting algorithmsActa Informatica, 1978