Abstract
In this paper we investigated a special resolution variant, based on an A-ordering, which decides some classes of clause sets. We think that similiar mechanisms may be defined to provide decision algorithms for other interesting classes of clause sets. We shall inquire along this line of arguments into extensions of the Maslov class (i.e. the class of formulas with prefix of type ∀*∃* and at most two literals in each disjunct) in a forthcoming paper.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Dreben, B., and Goldfarb, W.D., The Decision Problem. Addison-Wesley, Massachusetts 1979.
Fermüller, C., Deciding some Horn Clause Sets by Resolution. Yearbook of the Kurt Gödel Society 1989, pp. 60–73.
Joyner, W.H., Resolution Strategies as Decision Procedures. J. ACM 23,1 (July 1976), pp. 398–417.
Kowalski, R., and Hayes P.J., Semantic trees in automated theorem proving in Machine Intelligence 4, B. Meltzer and D. Michie, Eds., Edinburgh U. Press, Edinburgh 1969, pp. 87–101.
Leitsch, A., Deciding Horn Classes by Hyperresolution. Proc. of the CSL '89, LNCS 440, pp. 225–241.
Lewis, H.R., Unsolvable Classes of Quantificational Formulas. Addison-Wesley, Massachusetts 1979.
Loveland, D., Automated Theorem Proving: A Logical Basis. North Holland, Amsterdam 1978.
Maslov, S. Ju., An Inverse Method of Establishing Deducability in the Classical Predicate Calculus. Soviet Math.-Doklady 5 (1964), pp. 1420–1424 (translated).
Maslov, S.Ju., Proof-search Strategies for Methods of the Resolution Type. Machine Intelligence 6, American Elsevier, 1971, pp. 77–90.
Nilson, N.J., Problem-Solving Methods in Artificial Intelligence. McGraw-Hill, New York, 1971.
Robinson, J.A., A Machine-oriented Logic Based on the Resolution Principle. J. ACM 12,1 (Jan. 1965), pp. 23–41.
Tammet, T., A Resolution Program, Able to Decide some Solvable Classes. Proc. of the COLOG '88, LNCS 417, pp. 300–311.
Zamov, N.K., Maslov's Inverse Method and Decidable Classes. Annals of Pure and Applied Logic 42 (1989), pp. 165–194.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fermüller, C. (1991). A resolution variant deciding some classes of clause sets. In: Börger, E., Kleine Büning, H., Richter, M.M., Schönfeld, W. (eds) Computer Science Logic. CSL 1990. Lecture Notes in Computer Science, vol 533. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54487-9_56
Download citation
DOI: https://doi.org/10.1007/3-540-54487-9_56
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54487-6
Online ISBN: 978-3-540-38401-4
eBook Packages: Springer Book Archive