Abstract
In the first part of the paper we describe our theorem-prover implementing a certain modification of the resolution strategy of N.Zamov. Zamov's strategy decides a number of solvable classes, including Maslov's Class K (this class contains most well-known decidable classes like Gödel's Class, Skolem's Class, Monadic Class). We describe several experiments performed with the theorem-prover.
The second part of a paper consists of a proof that a presented modoification of Zamov's strategy decides a wide class of formulas with functional symbols, called E+.
The work described here has been guided by G.Mints. We would also like to thank N.Zamov for helpful discussions.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Church, A. Introduction to mathematical logic I. (Princeton University Press, New Jersey, 1956).
Dreben, B., Goldfarb, W.D. The decision problem: solvable classes of quantificational formulas. (Addison-Wesley, Reading, 1979).
Hindley, R., Meredith, D. Principal type-schemes and condensed detachment. Preprint, October 1987.
Joyner, W.H. Resolution strategies as decision procedures. J. ACM 23 (3)(1976), 396–417.
Leitsch, A. On different concepts of resolution. Zeitschr. f. math. Logik und Grundlagen d. Math. 35 (1989) 71–77.
Maslov, S.Ju. An inverse method of establishing deducibility in the classical predicate calculus. Dokl. Akad. Nauk. SSSR 159 (1964) 17–20=Soviet Math. Dokl. 5 (1964) 1420, MR 30 #3005.
Maslov, S.Ju. The inverse method for establishing deducibility for logical calculi. Trudy Mat. Inst. Steklov 98 (1968) 26–87=Proc. Steklov. Inst. Math. 98 (1968) 25–96, MR 40 #5416; 43 #4620.
Maslov, S.Ju. Proof-search strategies for methods of the resolution type. Machine Intelligence 6 (American Elsevier, 1971) 77–90.
Mints, G.E, Tammet, T. Experiments in proving formulas of non-classical logics with a resolution theorem-prover. To appear.
Wos, L., Overbeek, R., Lusk, E. Boyle, J. Automated reasoning: introduction and applications. (Prentice-Hall, New Jersey, 1984).
Zamov, N.K., On a bound for the complexity of terms in the resolution method. Trudy Mat. Inst. Steklov 128 (1972), 5–13.
Zamov, N.K., Maslov's inverse method and decidable classes. Annals of Pure and Applied Logic 42 (1989), 165–194.
Маслов С. Ю, Минц Г.Е. Теория поиска вывода и обратныи метод. Доп. к русскому переводу: Чень, Ч., Ли, Р. математическая логика и автоматическое доказательство теорем. (Наука, М., 1983) 291–314.
Оревков В.П. Один разрешимый классс формул классического исчисления предикатов с функционалными знаками. Сб: II симпозиум по кибернетике (тезисы), Тбилиси 1965, 176.
Сочилина А. В. О программе, реализующей алгоритм установления выводимости формул классического исчисления предикатов. Семиотика и информатика 12 (1979).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tammet, T. (1990). The resolution program, able to decide some solvable classes. In: Martin-Löf, P., Mints, G. (eds) COLOG-88. COLOG 1988. Lecture Notes in Computer Science, vol 417. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52335-9_61
Download citation
DOI: https://doi.org/10.1007/3-540-52335-9_61
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52335-2
Online ISBN: 978-3-540-46963-6
eBook Packages: Springer Book Archive