Abstract
Certain aspects of the theorem proving system TPS are described. Type theory with λ-abstraction has been chosen as the logical language of TPS so that statements from many fields of mathematics and other disciplines can be expressed in terms accessible to the system.
Considerable effort has been devoted to making TPS a useful research tool with which interaction is efficient and convenient. Numerous special characters are available on the terminals and printer used by TPS, and many of the traditional notations of mathematics and logic can be used in interactions with the system. When constructing a proof interactively, the user needs to specify only essential information, and can often construct needed wffs from others already present with the aid of a flexible editor for wffs.
TPS constructs proofs in natural deduction style and as p-acceptable matings. Proofs in the latter style can be automatically converted to the former. TPS can be used in a mixture of interactive and automatic modes, so that human input need be given only at critical points in the proof.
The implementations of the algorithms which search for matings and perform higher order unification are described, along with some associated search heuristics. One heuristic used in the search for matings, of special value for dealing with wffs containing equality, considers in close sequence vertical paths on which mating processes are likely to interact. A very useful heuristic for pruning unification trees involves deleting nodes subsumed by other nodes. It is shown how the unification procedure deals with unification problems which keep growing as the search for a mating progresses.
It has been found that although unification of literals is more complicated for higher order logic than for first order logic, this is not a major source of difficulty.
An example is given to show how TPS constructs a proof.
This work is supported by NSF Grants MCS78-01462 and MCS81 -02870.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Peter B. Andrews, “Transforming Matings into Natural Deduction Proofs,” in 5th Conference on Automated Deduction, Les Arcs, France, edited by W. Bibel and R. Kowalski, Lecture Notes in Computer Science, No. 87, Springer-Verlag, 1980, 281–292.
Peter B. Andrews, Theorem Proving via General Matings, Journal of the Association for Computing Machinery 28 (1981), 193–214.
Alonzo Church, A Formulation of the Simple Theory of Types, Journal of Symbolic Logic 5 (1940), 56–68.
Gérard P. Huet, A Unification Algorithm for Typed λ-Calculus, Theoretical Computer Science 1 (1975), 27–57.
Gérard Huet, Resolution d'Équations dans les Languages d'Ordre 1,2,..., ω, Thèse de Doctorat D'État, Université Paris VII, 1976.
D. C. Jensen and T. Pietrzykowski, Mechanizing ω-Order Type Theory Through Unification, Theoretical Computer Science 3 (1976), 123–171.
Brian K. Reid and Janet H. Walker, SCRIBE Introductory User's Manual, Third edition, UNILOGIC, Ltd., 160 N. Craig St., Pittsburgh, PA 15213, 1980.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1982 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Miller, D.A., Cohen, E.L., Andrews, P.B. (1982). A look at TPS. In: Loveland, D.W. (eds) 6th Conference on Automated Deduction. CADE 1982. Lecture Notes in Computer Science, vol 138. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0000051
Download citation
DOI: https://doi.org/10.1007/BFb0000051
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-11558-8
Online ISBN: 978-3-540-39240-8
eBook Packages: Springer Book Archive