{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:19:13Z","timestamp":1725455953208},"publisher-location":"Berlin\/Heidelberg","reference-count":20,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540541314"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0019355","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T05:26:33Z","timestamp":1132637193000},"page":"33-64","source":"Crossref","is-referenced-by-count":13,"title":["Using resolution for deciding solvable classes and building finite models"],"prefix":"10.1007","author":[{"given":"Tanel","family":"Tammet","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","volume-title":"The Lambda Calculus","author":"H.P. Barendregt","year":"1981","unstructured":"Barendregt, H.P. The Lambda Calculus. (North Holland, Amsterdam, 1981)."},{"key":"3_CR2","volume-title":"Introduction to mathematical logic I.","author":"A. Church","year":"1956","unstructured":"Church, A. Introduction to mathematical logic I. (Princeton University Press, New Jersey, 1956)."},{"key":"3_CR3","volume-title":"The decision problem: solvable classes of quantificational formulas","author":"B. Dreben","year":"1979","unstructured":"Dreben, B., Goldfarb, W.D. The decision problem: solvable classes of quantificational formulas. (Addison-Wesley, Reading, 1979)."},{"issue":"3","key":"3_CR4","doi-asserted-by":"crossref","first-page":"396","DOI":"10.1145\/321958.321960","volume":"23","author":"W.H. Joyner","year":"1976","unstructured":"Joyner, W.H. Resolution strategies as decision procedures. J. ACM 23 (3) (1976), 396\u2013417.","journal-title":"J. ACM"},{"key":"3_CR5","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1002\/malq.19890350109","volume":"35","author":"A. Leitsch","year":"1989","unstructured":"Leitsch, A. On different concepts of resolution. Zeitschr. f. math. Logik und Grundlagen d. Math. 35 (1989) 71\u201377.","journal-title":"Zeitschr. f. math. Logik und Grundlagen d. Math."},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Leitsch, A. Implication algorithms for classes of horn clauses. Statistik, Informatik und \u00d6konomie, hrsg. v. W.Janko. 172\u2013189, Springer 1988.","DOI":"10.1007\/978-3-642-74052-7_14"},{"issue":"3","key":"3_CR7","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/0022-0000(80)90027-6","volume":"21","author":"H.R. Lewis","year":"1980","unstructured":"Lewis, H.R. Complexity results for classes of quantificational formulas. J. Computer and System Sciences 21 (3) (1980) 317\u2013353","journal-title":"J. Computer and System Sciences"},{"key":"3_CR8","first-page":"17","volume":"159","author":"S. Maslov","year":"1964","unstructured":"Maslov, S.Ju. An inverse method of establishing deducibility in the classical predicate calculus. Dokl. Akad. Nauk. SSSR 159 (1964) 17\u201320=Soviet Math. Dokl. 5 (1964) 1420, MR 30 #3005.","journal-title":"Dokl. Akad. Nauk. SSSR"},{"key":"3_CR9","first-page":"26","volume":"98","author":"S. Maslov","year":"1968","unstructured":"Maslov, S.Ju. The inverse method for establishing deducibility for logical calculi. Trudy Mat. Inst. Steklov 98 (1968) 26\u201387= Proc. Steklov. Inst. Math. 98 (1968) 25\u201396, MR 40 #5416; 43 #4620.","journal-title":"Trudy Mat. Inst. Steklov"},{"key":"3_CR10","first-page":"77","volume":"6","author":"S. Maslov","year":"1971","unstructured":"Maslov, S.Ju. Proof-search strategies for methods of the resolution type. Machine Intelligence 6 (American Elsevier, 1971) 77\u201390.","journal-title":"Machine Intelligence"},{"key":"3_CR11","unstructured":"Mints, G.E, Tammet, T. Experiments in proving formulas of nonclassical logics with a resolution theorem-prover. To appear in the Journal of Automated Reasoning."},{"issue":"4","key":"3_CR12","doi-asserted-by":"publisher","first-page":"622","DOI":"10.1145\/321850.321859","volume":"21","author":"J.R. Slagle","year":"1974","unstructured":"Slagle, J.R. Automated theorem-proving for theories with simplifiers, commutativity and associativity. J. ACM 21 (4) (1974), 622\u2013642.","journal-title":"J. ACM"},{"key":"3_CR13","first-page":"300","volume":"417","author":"T. Tammet","year":"1990","unstructured":"Tammet, T. A resolution program, able to decide some solvable classes. Proceedings of Colog-88, LNCS 417, 300\u2013312, Springer Verlag 1990.","journal-title":"LNCS"},{"key":"3_CR14","volume-title":"Automated reasoning: introduction and applications","author":"L. Wos","year":"1984","unstructured":"Wos, L., Overbeek, R., Lusk, E. Boyle, J. Automated reasoning: introduction and applications. (Prentice-Hall, New Jersey, 1984)."},{"key":"3_CR15","first-page":"5","volume":"128","author":"N.K. Zamov","year":"1972","unstructured":"Zamov, N.K., On a bound for the complexity of terms in the resolution method. Trudy Mat. Inst. Steklov 128 (1972), 5\u201313.","journal-title":"Trudy Mat. Inst. Steklov"},{"key":"3_CR16","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/0168-0072(89)90053-5","volume":"42","author":"N.K. Zamov","year":"1989","unstructured":"Zamov, N.K., Maslov's inverse method and decidable classes. Annals of Pure and Applied Logic 42 (1989), 165\u2013194.","journal-title":"Annals of Pure and Applied Logic"},{"key":"3_CR17","unstructured":"\u041c\u0430\u0441\u043b\u043e\u0432 \u0421.\u042e. \u041c\u0438\u043d\u0446 \u0413.\u0415. \u0422\u0435\u043e\u0440\u0438\u044f \u043f\u043e\u0438\u0441\u043a\u0430 \u0432\u044b\u0432\u043e\u0434\u0430 \u0438 \u043e\u0431\u0440\u0430\u0442\u043d\u044b\u0439 \u043c\u0435\u0442\u043e\u0434. \u0414\u043e\u043f. \u043a \u0440\u0443\u0441\u0441\u043a\u043e\u043c\u0443 \u043f\u0435\u0440\u0435\u0432\u043e\u0434\u0443: \u0427\u0435\u043d\u044c, \u0427., \u041b\u0438, \u0420. \u041c\u0430\u0442\u0435\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0430\u044f \u043b\u043e\u043e\u0433\u0438\u043a\u0430 \u0438 \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u0435 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u043e \u0442\u0435\u043e\u0440\u0435\u043c. (\u041d\u0430\u0443\u043a\u0430, \u041c., 1983) 291\u2013314."},{"key":"3_CR18","unstructured":"\u041e\u0440\u0435\u0432\u043a\u043e\u0432 \u0412.\u041f. \u041e\u0434\u0438\u043d \u0440\u0430\u0437\u0440\u0435\u0449\u0438\u043c\u044b\u0439 \u043a\u043b\u0430\u0441\u0441 \u0444\u043e\u0440\u043c\u0443\u043b \u043a\u043b\u0430\u0441\u0441\u0438\u0447\u0435\u0441\u043a\u043e\u0433\u043e \u0438\u0441\u0447\u0438\u0441\u043b\u0435\u043d\u0438\u044f \u043f\u0440\u0435\u0434\u0438\u043a\u0430\u0442\u043e\u0432 \u0441 \u0444\u0443\u043d\u043a\u0446\u0438\u043e\u043d\u0430\u043b\u044c\u043d\u044b\u043c\u0438 \u0437\u043d\u0430\u043a\u0430\u043c\u0438. \u0421\u0411: II \u0441\u0438\u043c\u043f\u043e\u0437\u0438\u0443\u043c \u043f\u043e \u043a\u0438\u0431\u0435\u0440\u043d\u0435\u0442\u0438\u043a\u0435 (\u0442\u0435\u0437\u0438\u0441\u044b), \u0442\u0431\u0438\u043b\u0438\u0441\u0438 1965, 176."},{"key":"3_CR19","unstructured":"\u0421\u043e\u0447\u0438\u043b\u0438\u043d\u0430 \u0410.\u0412. \u041e \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0435, \u0440\u0435\u0430\u043b\u0438\u0437\u0443\u044e\u0449\u0435\u0439 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u0443\u0441\u0442\u0430\u043d\u043e\u0432\u043b\u0435\u043d\u0438\u044f \u0432\u044b\u0432\u043e\u0434\u0438\u043c\u043e\u0441\u0442\u0438 \u0444\u043e\u0440\u043c\u0443\u043b \u043a\u043b\u0430\u0441\u0441\u0438\u0447\u0435\u0441\u043a\u043e\u0433\u043e \u0438\u0441\u0447\u0438\u0441\u043b\u0435\u043d\u0438\u044f \u043f\u0440\u0435\u0434\u0438\u043a\u0430\u0442\u043e\u0432. \u0421\u0435\u043c\u0438\u043e\u0442\u0438\u043a\u0430 \u0438 \u0438\u043d\u0444\u043e\u0440\u043c\u0430\u0442\u0438\u043a\u0430 12 (1979)."},{"key":"3_CR20","unstructured":"\u0428\u0430\u0440\u043e\u043d\u043e\u0432 \u0412.\u0418. \u0410\u043d\u0430\u043b\u0438\u0437 \u043f\u043e\u043b\u043d\u043e\u0442\u044b \u0441\u0442\u0440\u0430\u0442\u0435\u0433\u0438\u0439 \u0432 \u043c\u0435\u0442\u043e\u0434\u0435 \u0440\u0435\u0437\u043e\u043b\u044e\u0446\u0438\u0439. \u0414\u0438\u0441\u0441\u0435\u0440\u0442\u0430\u0446\u0438\u044f. \u041b\u0435\u043d\u0438\u043d\u0433\u0440\u0430\u0434 1973."}],"container-title":["Lecture Notes in Computer Science","Baltic Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0019355.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T21:42:13Z","timestamp":1607550133000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0019355"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540541314"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/bfb0019355","relation":{},"subject":[]}}