Abstract
In [8] J. A. Robinson introduced a complete refutation procedure called resolution for first order predicate calculus. Resolution is based on ideas in Herbrand’s Theorem, and provides a very convenient framework in which to search for a proof of a wff believed to be a theorem. Moreover, it has proved possible to formulate many refinements of resolution which are still complete but are more efficient, at least in many contexts. However, when efficiency is a prime consideration, the restriction to first order logic is unfortunate, since many statements of mathematics (and other disciplines) can be expressed more simply and naturally in higher order logic than in first order logic. Also, the fact that in higher order logic (as in many-sorted first order logic) there is an explicit syntactic distinction between expressions which denote different types of intuitive objects is of great value where matching is involved, since one is automatically prevented from trying to make certain inappropriate matches. (One may contrast this with the situation in which mathematical statements are expressed in the symbolism of axiomatic set theory.)
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Peter B. Andrews, “Resolution and the Consistency of Analysis”, Notre Dame Journal of Formal Logic XV (1974), 73–84.
Peter B. Andrews, “Provability in Elementary Type Theory”, Zeitschrift für Mathematische Logic und Grundlagen der Mathematik 20 (1974), 411–418.
Gérard P. Huet, “A Unification Algorithm for Typed,Calculus”, Theoretical Computer Science 1 (1975), 27–57.
D.C. Jensen and T. Pietrzykowski, “Mechanizing car-order Type Theory Through Unification”, Theoretical Computer Science 3 (1976), 123–171.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1971 Association for Symbolic Logic
About this chapter
Cite this chapter
Andrews, P.B. (1971). Resolution in Type Theory. In: Siekmann, J.H., Wrightson, G. (eds) Automation of Reasoning. Symbolic Computation. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-81955-1_29
Download citation
DOI: https://doi.org/10.1007/978-3-642-81955-1_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-81957-5
Online ISBN: 978-3-642-81955-1
eBook Packages: Springer Book Archive