Resolution Strategies as Decision Procedures

Abstract

The resolution principle, an automatic inference technique, is studied as a possible decision procedure for certain classes of first-order formulas. It is shown that most previous resolution strategies do not decide satisfiability even for “simple” solvable classes. Two new resolution procedures are described and are shown to be complete (i.e. semidecision procedures) in the general case and, in addition, to be decision procedures for successively wider classes of first-order formulas. These include many previously studied solvable classes. The proofs that a complete resolution procedure will always halt (without producing the empty clause) when applied to satisfiable formulas in certain classes provide new, and in some cases more enlightening, demonstrations of the solvability of these classes. A technique for constructing a model for a formula shown satisfiable in this way is also described.

References

1. 1 AANDERAA, S O , AND LEWIS, H R Linear samphng and the VbV case of the decision problem J Symbohe Logic 39, 3 (Sept 1974), 519-548
2. 2 ACKERMANN, W Solvable Cases of the Decision Problem North-Holland Pub Co , Amsterdam, 1954
3. 3 ANDREWS, P B ResoIutlon with merging J ACM 15, 3 (July 1968), 367-381
4. 4 CHANG, C L , AND LEE, R C T Symbolic Logic and Mechamcal Theorem Proving Academic Press, New York, 1973.
5. 5 CHURCH, A A note on the Entscheldungsprobiem J Symbolzc Logzc i (1936), 40-41, 101-102
6. 6 CHURCH, A. Introduction to MathematteaILogzc, Vol I Princeton U Press, Princeton, NJ , 1956
7. 7 DREBEN, B Solvable Surdmyl subclasses: An introduction to the Herhrand theory Annals of the Computation Lab of Harvard University, Vol XXXI, Harvard U Press, Cambridge, Mass , 1962, pp 32-47
8. 8 DREBEN, B , AND GOLDFARB, W D A Systematic Treatment of the Decision Problem (forthcoming)
9. 9 FRIEDMAN, J A semi-decision procedure for the functional calculus J ACM 10, 1 (Jan 1963), 1- 24
10. 10 HERBRAND, J. Recherches sur la thorle de la demonstratmn Thesis, U of Paris, Paris, 1930, partially translated m {33}
11. 11 JOYNZR, W H Automatic theorem-proving and the decision problem Tech Rep 7-73, Center for Research m Computing Technology, Harvard U , Cambridge, Mass , 1073
12. 12 JOYNER, W H Automatic theorem prowng and the decision problem, 14th Annual Syrup on Switching and Automata Theory, Iowa City, Iowa, 1973, 159-166
13. 13 KAHR, A S , MOORE, E F , AND WANG, H Entscheldungsproblem reduced to the AEA case Proc Nat Acad Sc 48 (1962), 365-377
14. 14 KALLICK, B A declsmn procedure based on the resolution method Proc IFIP Cong 1968, North- Holland Pub Co, Amsterdam, pp 269-275
15. 15 KOWALSKI, R , AND HAYES, P J Semantic trees in automatic theorem-proving In Machine Intelhgence 4, B Meltzer and D Mlchle, Eds , Edinburgh U Press, Edinburgh, 1969, pp 87-101
16. 16 KOWALSKI, R , AND KUEHNER, D L1near resolution with selection function Artificial Intellzgence 2 (1971), 227-260
17. 17 KROM, M R The declsmn problem for formulas in prenex conjunctive normal form with binary disjunctions J Symbohc Logw 35 (1970), 210-216
18. 18 LEwis, H R Program schemata and the first-order decision problem J Comput Syst Scts 8, 1 (Feb 1974), 71-83
19. 19 LOVELAND, D A linear format for resolution Proc IRIA Syrup on Automatic Demonstration, Lecture Notes in Mathematics No 125, Springer-Verlag, New York, 1970, pp 147-162
20. 20 LOWENHEIM, L Uber Moghchkelten am Relatlvkalkul Mathematsche Annalen 76 (1915), 447- 470 Translated in {33}
21. 21 LUCKHAM, D Refinement theorems in resolution theory Proc. IRIA Symp on Automahc Demonstration, Lecture Notes in Mathematics No 125, Springer-Verlag, New York, 1970, pp 163-190
22. 22 LUCKHAM, D , AND NILSSON, N J Extracting reformation from resolution proof trees Arttfictal InteUtgence 2 (1971), 27-54
23. 23 MANNA, Z Properties of programs and the first-order predicate calculus J ACM 16, 2 (April 1969), 244-255
24. 24 MASLOV. S J u An reverse method of establishing deduclblhty an the classical predicate calculus Sovtet Math -Doklady 5 (1964), 1420-1424 (translated)
25. 25 NILSSON, N J Problem-Solvtng Methods tn Arttficml lntelhgence McGraw-Hill, New York, 1971
26. 26 OBEVKOV, V P Two undecidable classes of formulas in classical predicate calculus. Seminars in Math, Vol 16, V A Steklov Inst , Leningrad, 1969, pp 98-102 (translated)
27. 27 ROBINSON, G , AND WoN, L Paramodulatlon and theorem-proving m first order theories with equality Machtne Intelhgence 4, B Meltzer and D Mlchie, Eds , Edinburgh U Press, Edinburgh, 1969, pp 135-150
28. 28 ROBINSON, J A A machine-oriented logic based on the resolution principle J ACM 12, 1 (Jan 1965), 23-41
29. 29 ROBINSON. J A Automatic deduction with hyperresolutlon lnt J Comput Math 1 (1965), 227- 234
30. 30 ROBINSON, J A The generahzed resolutmn principle In Machtne Intelhgence 3, D Mlchle, E d , Edinburgh U Press, Edinburgh, 1968, pp 77-93
31. 31 SURANYI, J Zur Reduktlon des Entscheldungsproblem des loglschen Funktionenkalkuls Matemattkat es Ftztkat Lapok 50 (1943), 51-74
32. 32 TUBING, A M On computable numbers, with an application to the Entscheldungsproblem Proc London Math Soc 42 (1937), 230-265, 43 (1937), 544-546
33. 33 VAN HEIJENOORT, J , Ed From Frege to Godel A Source Book tn Mathematzcal Logtc 1879-1931 Harvard U Press, Cambridge, Mass , 1967

Index Terms

• Computing methodologies

  • Artificial intelligence

    • Knowledge representation and reasoning

  • Machine learning

    • Machine learning approaches

      • Markov decision processes

• Mathematics of computing

  • Probability and statistics

    • Probabilistic representations

      • Decision diagrams

• Theory of computation

  • Computational complexity and cryptography

    • Oracles and decision trees

  • Theory and algorithms for application domains

    • Machine learning theory

      • Markov decision processes

      • Reinforcement learning

        • Sequential decision making