{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:22:42Z","timestamp":1725456162672},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540600176"},{"type":"electronic","value":"9783540494041"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0022265","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T01:12:29Z","timestamp":1132621949000},"page":"309-323","source":"Crossref","is-referenced-by-count":0,"title":["Completeness of resolution for definite answers with case analysis"],"prefix":"10.1007","author":[{"given":"Tanel","family":"Tammet","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,15]]},"reference":[{"key":"23_CR1","unstructured":"C.L.Chang, R.C.T Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973."},{"issue":"N4","key":"23_CR2","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1145\/360924.360967","volume":"17","author":"C.L. Chang","year":"1974","unstructured":"C.L.Chang, R.C.T. Lee, R.Waldinger. An Improved Program-Synthesizing Algorithm and its Correctness. Comm. of ACM, (1974), V17, N4, 211\u2013217.","journal-title":"Comm. of ACM"},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"C.Ferm\u00fcller, A.Leitsch, T.Tammet, N.Zamov. Resolution Methods for the Decision Problem. Lecture Notes in Artificial Intelligence 679, Springer Verlag, 1993.","DOI":"10.1007\/3-540-56732-1"},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"C.Green. Application of theorem-proving to problem solving. In Proc. 1st Internat. Joint. Conf. Artificial Intelligence, pages 219\u2013239, 1969.","DOI":"10.21236\/ADA459656"},{"key":"23_CR5","volume-title":"Introduction to Metamathematics","author":"S.C. Kleene","year":"1952","unstructured":"S.C.Kleene. Introduction to Metamathematics. North-Holland, Amsterdam, 1952."},{"issue":"1","key":"23_CR6","first-page":"91","volume":"N2","author":"Z. Manna","year":"1980","unstructured":"Z.Manna, R.Waldinger. A deductive approach to program synthesis. ACM Trans. Programming Languages and Systems, (1980), N2(1), 91\u2013121.","journal-title":"ACM Trans. Programming Languages and Systems"},{"issue":"N8","key":"23_CR7","doi-asserted-by":"publisher","first-page":"674","DOI":"10.1109\/32.153379","volume":"18","author":"Z. Manna","year":"1992","unstructured":"Z.Manna, R.Waldinger. Fundamentals of Deductive Program Synthesis. IEEE Transactions on Software Engineering, (1992), V18, N8, 674\u2013704.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"23_CR8","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1016\/0167-6423(83)90016-3","volume":"N2","author":"G. Mints","year":"1982","unstructured":"G.Mints, E.Tyugu. Justification of the structural synthesis of programs. Sci. of Comput. Program., (1982), N2, 215\u2013240.","journal-title":"Sci. of Comput. Program."},{"key":"23_CR9","doi-asserted-by":"crossref","unstructured":"G.Mints. Gentzen-type Systems and Resolution Rules. Part I. Prepositional Logic. In COLOG-88, pages 198\u2013231. Lecture Notes in Computer Science vol. 417, Springer Verlag, 1990.","DOI":"10.1007\/3-540-52335-9_55"},{"key":"23_CR10","unstructured":"G.Mints. Gentzen-type Systems and Resolution Rules. Part II. Predicate Logic. In Logic Colloquium '90."},{"key":"23_CR11","volume-title":"Programming in Martin-L\u00f6fs Type Theory","author":"B. Nordstr\u00f6m","year":"1990","unstructured":"B.Nordstr\u00f6m, K.Petersson, J.M.Smith. Programming in Martin-L\u00f6fs Type Theory. Clarendon Press, Oxford, 1990."},{"key":"23_CR12","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1137\/0212006","volume":"N12","author":"G. Peterson","year":"1983","unstructured":"G.Peterson. A technique for establishing completeness results in theorem proving with equality. SIAM J. of Comput. (1983), N12, 82\u2013100.","journal-title":"SIAM J. of Comput."},{"key":"23_CR13","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"J.A. Robinson. A Machine-oriented Logic Based on the Resolution Principle. Journal of the ACM 12, 1965, pp 23\u201341.","journal-title":"Journal of the ACM"},{"key":"23_CR14","unstructured":"U.R.Schmerl. A Resolution Calculus Giving Definite Answers. Report Nr 9108, July 1991, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t der Bundeswehr M\u00fcnchen."},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"N.Shankar. Proof Search in the Intuitionistic Sequent Calculus. In CADE-11, pages 522\u2013536, Lecture Notes in Artificial Intelligence 607, Springer Verlag, 1992.","DOI":"10.1007\/3-540-55602-8_189"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0022265","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,5]],"date-time":"2019-02-05T02:17:13Z","timestamp":1549333033000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0022265"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540600176","9783540494041"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/bfb0022265","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}