Advertisement

A resolution variant deciding some classes of clause sets

  • Christian Fermüller
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 533)

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.

Keywords

Decision Procedure Predicate Symbol Functional Term Ground Atom Resolution Variant 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    Dreben, B., and Goldfarb, W.D., The Decision Problem. Addison-Wesley, Massachusetts 1979.Google Scholar
  2. [2]
    Fermüller, C., Deciding some Horn Clause Sets by Resolution. Yearbook of the Kurt Gödel Society 1989, pp. 60–73.Google Scholar
  3. [3]
    Joyner, W.H., Resolution Strategies as Decision Procedures. J. ACM 23,1 (July 1976), pp. 398–417.CrossRefGoogle Scholar
  4. [4]
    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
  5. [5]
    Leitsch, A., Deciding Horn Classes by Hyperresolution. Proc. of the CSL '89, LNCS 440, pp. 225–241.Google Scholar
  6. [6]
    Lewis, H.R., Unsolvable Classes of Quantificational Formulas. Addison-Wesley, Massachusetts 1979.Google Scholar
  7. [7]
    Loveland, D., Automated Theorem Proving: A Logical Basis. North Holland, Amsterdam 1978.Google Scholar
  8. [8]
    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
  9. [9]
    Maslov, S.Ju., Proof-search Strategies for Methods of the Resolution Type. Machine Intelligence 6, American Elsevier, 1971, pp. 77–90.Google Scholar
  10. [10]
    Nilson, N.J., Problem-Solving Methods in Artificial Intelligence. McGraw-Hill, New York, 1971.Google Scholar
  11. [11]
    Robinson, J.A., A Machine-oriented Logic Based on the Resolution Principle. J. ACM 12,1 (Jan. 1965), pp. 23–41.CrossRefGoogle Scholar
  12. [12]
    Tammet, T., A Resolution Program, Able to Decide some Solvable Classes. Proc. of the COLOG '88, LNCS 417, pp. 300–311.Google Scholar
  13. [13]
    Zamov, N.K., Maslov's Inverse Method and Decidable Classes. Annals of Pure and Applied Logic 42 (1989), pp. 165–194.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • Christian Fermüller
    • 1
  1. 1.Institut für Praktische InformatikTechnical University ViennaWien

Personalised recommendations