Abstract
We introduce a general notion of resolution calculus. We show that it is possible to obtain a resolution calculus from a semantic tableau calculus that can be described by rules of a certain type. It is also possible to obtain an ordered resolution calculus from a semantic tableau calculus. We apply this to classical logic to obtain simple proofs of the completeness of several refinements of resolution in classical logic.
Preview
Unable to display preview. Download preview PDF.
References
P. Baumgartner, An ordered theory resolution calculus, in LPAR92, Springer Verlag, Berlin, 1992.
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.
P. Enjalbert, L. Fariñas, Modal resolution in clausal form, theoretical computer science 65, 1989.
C. Fermüller, A. Leitsch, T. Tammet, N. Zamov, Resolution Methods for the decision problem, LNAI 679, Springer Verlag, 1993.
W. H. Joyner, Resolution Strategies as Decision Procedures, Journal of the association for computing machinery, vol. 23, 1976.
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, pp 198–231, Springer Verlag, 1988.
H. de Nivelle, A general resolution scheme, reports of the faculty of technical mathematics and informatics, no. 93–62, Delft, 1993.
H. de Nivelle, Generic resolution in propositional modal systems, in LPAR93, Springer Verlag, Berlin, 1993.
J.A. Robinson, A machine-oriented logic based on the resolution principle, Journal of the ACM, Vol. 12, No. 1, pp 23–41.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de Nivelle, H. (1994). A unification of ordering refinements of resolution in classical logic. In: MacNish, C., Pearce, D., Pereira, L.M. (eds) Logics in Artificial Intelligence. JELIA 1994. Lecture Notes in Computer Science, vol 838. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0021974
Download citation
DOI: https://doi.org/10.1007/BFb0021974
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58332-5
Online ISBN: 978-3-540-48657-2
eBook Packages: Springer Book Archive