A Science of Reasoning (Extended Abstract)

  • Alan Bundy
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1397)


How can we understand reasoning in general and mathematical proofs in particular? It is argued that a high-level understanding of proofs is needed to complement the low-level understanding provided by Logic. A role for computation is proposed to provide this high-level understanding, namely by the association of proof plans with proofs. Criteria are given for assessing the association of a proof plan with a proof.


Mathematical Proof Common Structure Logical Theory Inductive Proof Automate Deduction 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Benzmüller et al, 1997]_Benzmüller, C., Cheikhrouhou, L., Fehrer, D, Fiedler, A., Huang, X., Kerber, M., Kohlhase, K., Meirer, A, Melis, E., Schaarschmidt, W., Siekmann, J. and Sorge, V. (1997). Ωmega: Towards a mathematical assistant. In McCune, W., (ed.), 14th Conference on Automated Deduction, pages 252–255. Springer-Verlag.Google Scholar
  2. [Bledsoe et al, 1972]_Bledsoe, W. W., Boyer, R. S. and Henneman, W. H. (1972). Computer proofs of limit theorems. Artificial Intelligence, 3:27–60.zbMATHCrossRefMathSciNetGoogle Scholar
  3. [Bundy & Welham, 1981]
    Bundy, A. and Welham, B. (1981). Using meta-level inference for selective application of multiple rewrite rules in algebraic manipulation. Artificial Intelligence, 16(2):189–212. Also available from Edinburgh as DAI Research Paper 121.CrossRefMathSciNetGoogle Scholar
  4. [Bundy, 1988]
    Bundy, Alan. (1988). The use of explicit plans to guide inductive proofs. In Lusk, R. and Overbeek, R., (eds.), 9th Conference on Automated Deduction, pages 111–120. Springer-Verlag. Longer version available from Edinburgh as DAI Research Paper No. 349.Google Scholar
  5. [Bundy, 1991]
    Bundy, Alan. (1991). A science of reasoning. In Lassez, J.-L. and Plotkin, G., (eds.), Computational Logic: Essays in Honor of Alan Robinson, pages 178–198. MIT Press. Also available from Edinburgh as DAI Research Paper 445.Google Scholar
  6. [Bundy et al, 1988]_Bundy, A., van Harmelen, F., Hesketh, J. and Smaill, A. (1988). Experiments with proof plans for induction. Research Paper 413, Dept. of Artificial Intelligence, University of Edinburgh, Appeared in Journal of Automated Reasoning, 7, 1991.Google Scholar
  7. [Bundy et al, 1990]_Bundy, A., van Harmelen, F., Horn, C. and Smaill, A. (1990). The Oyster-Clam system. In Stickel, M. E., (ed.), 10th International Conference on Automated Deduction, pages 647–648. Springer-Verlag. Lecture Notes in Artificial Intelligence No. 449. Also available from Edinburgh as DAI Research Paper 507.Google Scholar
  8. [Funt, 1973]
    Funt, B. V. (October 1973). A procedural approach to constructions in Euclidean geometry. Unpublished M.Sc. thesis, University of British Columbia.Google Scholar
  9. [Gow, 1997]
    Gow, J. (1997). The Diagonalization Method in Automatic Proof. Under-graduate project dissertation, Dept of Artificial Intellience, University of Edinburgh.Google Scholar
  10. [Huang et al, 1995]_Huang, X., Kerber, M. and Cheikhrouhou. (1995). Adapting the diagonalization method by reformulations. In Levy, A. and Nayak, P., (eds.), Proc. of the Symposium on Abstraction, Reformulation and Approximation (SARA-95), pages 78–85. Ville d’Esterel, Canada.Google Scholar
  11. [Ireland & Bundy, 1996]
    Ireland, A. and Bundy, A. (1996). Productive use of failure in inductive proof. Journal of Automated Reasoning, 16(1–2):79–111. Also available as DAI Research Paper No 716, Dept. of Artificial Intelligence, Edinburgh.zbMATHCrossRefMathSciNetGoogle Scholar
  12. [Polya, 1965]
    Polya, G. (1965). Mathematical discovery. John Wiley & Sons, Inc, Two volumes.Google Scholar
  13. [Wos & McCune, 1988]
    Wos, L. and McCune, W. (1988). Searching for fixed point combinators by using automated theorem proving: a preliminary report. Technical Report ANL-88-10, Argonne National Laboratory.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Alan Bundy
    • 1
  1. 1.Department of Artificial IntelligenceUniversity of EdinburghEdinburghScotland

Personalised recommendations