Skip to main content
SpringerLink
Log in
Book cover

International Conference on Artificial Intelligence and Symbolic Mathematical Computing

AISMC 1994: Integrating Symbolic Mathematical Computation and Artificial Intelligence pp 48–63Cite as

Planning a proof of the intermediate value theorem

  • Conference paper
  • First Online:

  • 174 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 958))

Abstract

This paper descibes work done in The Mathematical Reasoning Group (MRG) in the Department of Artificial Intelligence at Edinburgh to allow the automatic proof of theorems in constructive analysis, with particular emphasis on the intermediate value theorem. This work included formalising theories of the rational and real numbers in a constructive type-theory and the development of meta-level tools to allow a proof of the theorem to be planned and constructed.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bishop, E. and Bridges, D.: Constructive Analysis. Springer-Verlag, 1985.

    Google Scholar 

  2. Bundy, A. and van Harmelen, F. and Smaill, A.: Extensions to the Rippling-Out Tactic for Guiding Inductive Proof. Proceedings of CADE-10.

    Google Scholar 

  3. Bundy, A.: The Use of Explicit Plans to Guide Inductive Proofs. Dept. of Artificial Intelligence, Edinburgh, Reaearch Paper 349.

    Google Scholar 

  4. Constable, R.L. and Allen, S.F. and Bromley, H.M. and others.: Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, 1986.

    Google Scholar 

  5. Nordström, B.S.: Terminating General Recursion. 1987.

    Google Scholar 

  6. van Harmelen, F. and Ireland, A. and Stevens, A. and Negrete, S.: The Clam Proof Planner, User Manual and Programmer Manual (version 1.5) Dept. of Artificial Intelligence, Edinburgh, 1992

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Rutherford Appleton Laboratory, Chilton, Didcot, Oxon

    Myles Chippendale

Authors
  1. Myles Chippendale
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jacques Calmet John A. Campbell

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Chippendale, M. (1995). Planning a proof of the intermediate value theorem. In: Calmet, J., Campbell, J.A. (eds) Integrating Symbolic Mathematical Computation and Artificial Intelligence. AISMC 1994. Lecture Notes in Computer Science, vol 958. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60156-2_5

Download citation

  • DOI: https://doi.org/10.1007/3-540-60156-2_5

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60156-2

  • Online ISBN: 978-3-540-49533-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation