Abstract
We prove the completeness of the combination of ordered resolution and factoring for a large class of non-liftable orderings, without the need for any additional rules, as for example saturation. This is possible because of a new proof method which avoids making use of the standard ordered lifting theorem. This new proof method is based on a new technique, which we call the resolution game.
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.
References
R.S. Boyer, Locking: A Restriction of Resolution, Ph. D. Thesis, University of Texas at Austin, Texas 1971.
C-L. Chang, R. C-T. Lee, Symbolic logic and mechanical theorem proving, Academic Press, New York 1973.
On Definitional Transformations to Normal Form for Intuitionistic Logic, unpublished.
C. Fermüller, A. Leitsch, T. Tammet, N. Zamov, Resolution Methods for the Decision Problem, Springer Verlag, 1993.
Jean H. Gallier, Logic for Computer Science, (Foundations of Automatic Theorem Proving), Harper & Row, Publishers, New York, 1986.
Linear Logic, in Theoretical Computer Science 50, pages 1–102, 1987.
J. Hsiang and M. Rusinowitch, Proving Refutational Completeness of Theorem-Proving Strategies: The Transfinite Semantic Tree Method, Journal of the ACM, Vol. 38, no. 3, July 1991, pp. 559–587.
W.H. Joyner, Resolution Strategies as Decision Procedures, J. ACM 23, 1 (July 1976), pp. 398–417.
R. Kowalski, P.J. Hayes, Semantic trees in automated theorem proving, Machine Intelligence 4, B. Meltzer and D. Michie, Edingburgh University Press, Edingburgh, 1969.
A. Leitsch, On Some Formal Problems in Resolution Theorem Proving, Yearbook of the Kurt Gödel Society, pp. 35–52, 1988.
D. W. Loveland, Automated Theorem Proving, a Logical Basis, North Holland Publishing Company, Amsterdam, New York, Oxford, 1978.
G. Mints, Gentzen-Type Systems and Resolution Rules, Part 1, Propositional Logic, in COLOG-88, International Conference on Computational Logic, Talinn (at that time) USSR, 1988.
H. de Nivelle, Resolution Games and Non-Liftable Resolution Orderings, Internal Report 94–36, Department of Mathematics and Computer Science, Delft University of Technology, 1994.
H. de Nivelle, Application of Resolution Games to Resolution Decision Procedures, Internal Report 94–50, Department of Mathematics and Computer Science, Delft University of Technology, 1994.
Resolution Games and Non-Liftable Resolution Orderings, in CSL 94, pp 279–293, Springer Verlag, Kazimierz, Poland, 1994
J. Reynolds, Unpublished Seminar Notes, Stanford University, Palo Alto, California, 1966.
J.A. Robinson, A Machine Oriented Logic Based on the Resolution Principle, Journal of the ACM, Vol. 12, pp 23–41, 1965.
R. Statman, Lower Bounds on Herbrand’s Theorem, in Proceedings of the American Mathematical Society, Vol. 75, Number 1, 1979.
T Tammet, Proof Search Strategies in Linear Logic, Report 70, Programming Methodology Group, Department of Computer Sciences, Chalmers University of Technology and University of Göteburg, 1993.
T Tammet, Separate Orderings for Ground and Non-Ground Literals Preserve Completeness of Resolution, unpublished, 1994.
N.K. Zamov: On a Bound for the Complexity of Terms in the Resolution Method, Trudy Mat. Inst. Steklóv 128, pp. 5–13, 1972.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1996 Springer-Verlag/Wien
About this paper
Cite this paper
de Nivelle, H. (1996). Resolution Games and Non-Liftable Resolution Orderings. In: Collegium Logicum. Collegium Logicum, vol 2. Springer, Vienna. https://doi.org/10.1007/978-3-7091-9461-4_1
Download citation
DOI: https://doi.org/10.1007/978-3-7091-9461-4_1
Publisher Name: Springer, Vienna
Print ISBN: 978-3-211-82796-3
Online ISBN: 978-3-7091-9461-4
eBook Packages: Springer Book Archive