Division of Informatics
Forrest Hill & 80 South Bridge
Research Paper #661 | |
|---|---|
| Title: | Proof Plans and Automatic Theorem Proving with Hints (Paper in Spanish) |
| Authors: | Negrete-Yankelevich,S |
| Date: | Aug 1993 |
| Presented: | To appear in the proceedings of the X conference of SMIA, Mexico City, September 1993 |
| Keywords: | |
| Abstract: | In mathematical text we often find exercises in which the author gives the student some hints to help him or her solve the hard steps of a proof. In this paper, we present the design and use of a system that allows us to incorporate hints in Automatic Theorem Proving in the context of the Proof Plans paradigm. This technique, developed by the Mathematical Reasoning Group at AI department, University of Edinburgh, consists of the generation of a proof plan from abstract specifications of proof techniques applicable in Proof Editors. The system introduced here allows us to incorporate the use of hints to generate proof plans in Clam, an implementation of Proof Plans used to proof theorems in Martin-Lof's type theory. The use of hints in Clam improves considerably its capacity as a development and experimentation environment for automatic theorem proving techniques. |
| Download: | NO ONLINE COPY |
![[Search These Pages]](http://www.dai.ed.ac.uk/icons/dai_search.gif){kind=icon}
![[DAI Home Page]](http://www.dai.ed.ac.uk/icons/dai_home.gif){kind=icon}
![[Comment]](http://www.dai.ed.ac.uk/icons/dai_comment.gif){kind=icon}