Abstract
When searching for proofs of theorems which contain definitions, it is a significant problem to decide which instances of the definitions to instantiate. We describe a method called dual instantiation, which is a partial solution to the problem in the context of the connection method; the same solution may also be adaptable to other search procedures. Dual instantiation has been implemented in TPS, a theorem prover for classical type theory, and we provide some examples of theorems that have been proven using this method. Dual instantiation has the desirable properties that the search for a proof cannot possibly fail due to insufficient instantiation of definitions, and that the natural deduction proof which results from a successful search will contain no unnecessary instantiations of definitions. Furthermore, the time taken by a proof search using dual instantiation is in general comparable to the time taken by a search in which exactly the required instances of each definition have been instantiated. We also describe how this technique can be applied to the problem of instantiating set variables.
This material is based upon work supported by the National Science Foundation under grant CCR-9624683. This work was supported in part by Intel Corporation through an equipment grant.
Preview
Unable to display preview. Download preview PDF.
References
Peter B. Andrews. Theorem Proving via General Matings. Journal of the ACM, 28:193–214, 1981.
Peter B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press, 1986.
Peter B. Andrews. On Connections and Higher-Order Logic. Journal of Automated Reasoning, 5:257–291, 1989.
Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, and Hongwei Xi. TPS: A Theorem Proving System for Classical Type Theory. Journal of Automated Reasoning, 16:321–353, 1996.
Sidney C. Bailin and Dave Barker-Plummer. Z-match: An Inference Rule for Incrementally Elaborating Set Instantiations. Journal of Automated Reasoning, 11:391–428, 1993. Errata: JAR 12:411–412, 1994.
Dave Barker-Plummer. Gazing: An Approach to the Problem of Definition and Lemma Use. Journal of Automated Reasoning, 8:311–344, 1992.
W. W. Bledsoe. Using Examples to Generate Instantiations of Set Variables. In Proceedings of IJCAI-83, Karlsruhe, Germany, pages 892–901, Aug 8–12, 1983.
W. W. Bledsoe and Peter Bruell. A Man-Machine Theorem-Proving System. Artificial Intelligence, 5(1):51–72, 1974.
W. W. Bledsoe and Gohui Feng. Set-Var. Journal of Automated Reasoning, 11:293–314, 1993.
Alonzo Church. A Formulation of the Simple Theory of Types. Journal of Symbolicogic, 5:56–68, 1940.
Fausto Giunchiglia and Adolfo Villafiorita. ABSFOL: a Proof Checker with Abstraction. In M.A. McRobbie and J.K. Slaney, editors, CADE-13: Proceedings of the 13th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 1104, pages 136–140. Springer-Verlag, 1996.
Fausto Giunchiglia and Toby Walsh. Theorem Proving with Definitions. In Proceedings of AISB 89, Society for the Study of Artificial Intelligence and Simulation of Behaviour, 1989.
Fausto Giunchiglia and Toby Walsh. A Theory of Abstraction. Artificial Intelligence, 57(2–3):323–389, 1992.
Gerard P. Huet. A Unification Algorithm for Typed λ-Calculus. Theoretical Computer Science, 1:27–57, 1975.
Ignace I. Kolodner. Fixed Points. American Mathematical Monthly, 71:906, 1964.
Dale A. Miller. A compact representation of proofs. Studia Logica, 46(4):347–370, 1987.
D. Pastre. Automatic Theorem Proving in Set Theory. Artificial Intelligence, 10:1–27, 1978
Frank Pfenning. Proof Transformations in Higher-Order Logic. PhD thesis, Carnegie Mellon University, 1987. 156 pp.
D.A. Plaisted. Abstraction Mappings in Mechanical Theorem Proving. In 5th Conference on Automated Deduction, Lecture Notes in Computer Science 87, pages 264–280. Springer-Verlag, 1980.
D.A. Plaisted. Theorem Proving with Abstraction. Artificial Intelligence, 16:47–108, 1981.
Dave Plummer. Gazing: Controlling the Use of Rewrite Rules. PhD thesis, Dept. of Artificial Intelligence, University of Edinburgh, 1987.
K. Warren. Implementation of a Definition Expansion Mechanism in a Connection Method Theorem Prover. Master's thesis, Dept. of Artificial Intelligence, Univ. of Edinburgh, 1987.
Larry Wos. The Problem of Definition Expansion and Contraction. Journal of Automated Reasoning, 3:433–435, 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bishop, M., Andrews, P.B. (1998). Selectively instantiating definitions. In: Kirchner, C., Kirchner, H. (eds) Automated Deduction — CADE-15. CADE 1998. Lecture Notes in Computer Science, vol 1421. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0054272
Download citation
DOI: https://doi.org/10.1007/BFb0054272
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64675-4
Online ISBN: 978-3-540-69110-5
eBook Packages: Springer Book Archive