Abstract
Most researchers consider the modern period of automated logic to have begun with the discovery of resolution by J.A. Robinson in 1963 at the Argonne National Laboratory. Previously, it was known by the Herbrand-Skolem-Godel theorem that semi-decision procedures could be designed for first-order logic by reducing the question of the unsatisfiability of a set of first-order formulae to the question of unsatisfiability of (roughly) a set of certain ground formulae derived from the original set in an effective way (for example, see [32]). But until Robinson invented the simple and powerful inference rule known as resolution [139], no practically efficient semi-decision procedure had been found. The crucial component of this seminal discovery was in fact the rediscovery by Robinson of the process of unification, which had been discovered by Herbrand in his thesis 33 years earlier (see Appendix 3).1
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1991 Springer Science+Business Media New York
About this chapter
Cite this chapter
Snyder, W. (1991). Introduction. In: A Proof Theory for General Unification. Progress in Computer Science and Applied Logic, vol 11. Birkhäuser, Boston, MA. https://doi.org/10.1007/978-1-4612-0435-0_1
Download citation
DOI: https://doi.org/10.1007/978-1-4612-0435-0_1
Publisher Name: Birkhäuser, Boston, MA
Print ISBN: 978-1-4612-6758-4
Online ISBN: 978-1-4612-0435-0
eBook Packages: Springer Book Archive