A resolution variant deciding some classes of clause sets
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.
KeywordsDecision Procedure Predicate Symbol Functional Term Ground Atom Resolution Variant
Unable to display preview. Download preview PDF.
- Dreben, B., and Goldfarb, W.D., The Decision Problem. Addison-Wesley, Massachusetts 1979.Google Scholar
- Fermüller, C., Deciding some Horn Clause Sets by Resolution. Yearbook of the Kurt Gödel Society 1989, pp. 60–73.Google Scholar
- 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.Google Scholar
- Leitsch, A., Deciding Horn Classes by Hyperresolution. Proc. of the CSL '89, LNCS 440, pp. 225–241.Google Scholar
- Lewis, H.R., Unsolvable Classes of Quantificational Formulas. Addison-Wesley, Massachusetts 1979.Google Scholar
- Loveland, D., Automated Theorem Proving: A Logical Basis. North Holland, Amsterdam 1978.Google Scholar
- Maslov, S. Ju., An Inverse Method of Establishing Deducability in the Classical Predicate Calculus. Soviet Math.-Doklady 5 (1964), pp. 1420–1424 (translated).Google Scholar
- Maslov, S.Ju., Proof-search Strategies for Methods of the Resolution Type. Machine Intelligence 6, American Elsevier, 1971, pp. 77–90.Google Scholar
- Nilson, N.J., Problem-Solving Methods in Artificial Intelligence. McGraw-Hill, New York, 1971.Google Scholar
- Tammet, T., A Resolution Program, Able to Decide some Solvable Classes. Proc. of the COLOG '88, LNCS 417, pp. 300–311.Google Scholar