{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T17:12:18Z","timestamp":1725729138535},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540545583"},{"type":"electronic","value":"9783662027110"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/978-3-662-02711-0_2","type":"book-chapter","created":{"date-parts":[[2013,6,4]],"date-time":"2013-06-04T08:52:52Z","timestamp":1370335972000},"page":"12-22","source":"Crossref","is-referenced-by-count":1,"title":["A Completeness Proof Technique for Resolution with Equality"],"prefix":"10.1007","author":[{"given":"Peter","family":"Baumgartner","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C Chang","year":"1973","unstructured":"C. Chang and R. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973."},{"key":"2_CR2","first-page":"107","volume-title":"Proc. GWAI\u201989","author":"U Furbach","year":"1989","unstructured":"U. Furbach, S. H\u00f6lldobler, and J. Schreiber. Paramodulation modulo equality. In Proc. GWAI\u201989, pages 107\u2013116. Springer, IFB 216, 1989."},{"key":"2_CR3","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/BF00248322","volume":"3","author":"U Furbach","year":"1989","unstructured":"Ulrich Furbach, Steffen H\u00f6lldobler, and Joachim Schreiber. Horn equational theories and paramodulation. Journal of Automated Reasoning, 3:309\u2013337, 1989.","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR4","volume-title":"Foundations of Equational Logic Programming","author":"H Steffen","year":"1989","unstructured":"Steffen H\u00f6lldbler. Foundations of Equational Logic Programming, volume 353 of Lecture Notes in Artificial Intelligence. Subseries of Lecture Notes in Computer Science. Springer, 1989."},{"key":"2_CR5","first-page":"54","volume-title":"Proc. ICALP\u201987","author":"J Hsiang","year":"1987","unstructured":"J. Hsiang and M. Rusinowitch. On word problems in equational theories. In Proc. ICALP\u201987, pages 54\u201371. Springer, LNCS 267, 1987."},{"key":"2_CR6","volume-title":"Machine Intelligence 5","author":"RA Kowalski","year":"1969","unstructured":"R.A. Kowalski and P. Hayes. Semantic Trees in Automatic Theorem Proving. In Meltzer and Mitchie, editors, Machine Intelligence 5. Edinburg University Press, 1969."},{"key":"2_CR7","first-page":"287","volume-title":"Proc. IJCAI","author":"JB Morris","year":"1969","unstructured":"J. B. Morris. E-Resolution: An Extension of Resolution to include the Equality Relation. In Proc. IJCAI, pages 287\u2013294, 1969."},{"issue":"1","key":"2_CR8","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1137\/0212006","volume":"12","author":"G Peterson","year":"1983","unstructured":"G. Peterson. A Technique for Establishing Completeness Results in Theorem Proving with Equality. SIAM Journal on Computing, 12(1):82\u2013100, February 1983.","journal-title":"SIAM Journal on Computing"},{"issue":"1","key":"2_CR9","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"J.A. Robinson. A machine-oriented logic based on the resolution principle. JACM, 12(1):23\u201341, January 1965.","journal-title":"JACM"},{"key":"2_CR10","volume-title":"Theory Resolution: Building in Nonequational Theories","author":"ME Stickel","year":"1983","unstructured":"M.E. Stickel. Theory Resolution: Building in Nonequational Theories. SRI International Research Report Technical Note 286, Artificial Intelligence Center, 1983."},{"key":"2_CR11","volume-title":"Theory Resolution: Building in Nonequational Theories. SRI International Research Report Technical Note 286","author":"ME Stickel","year":"1983","unstructured":"M.E. Stickel. Theory Resolution: Building in Nonequational Theories. SRI International Research Report Technical Note 286, Artificial Intelligence Center, 1983."},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"M. E. Stickel. Automated deduction by theory resolution. Journal of Automated Reasoning, pages 333\u2013356, 1985.","DOI":"10.1007\/BF00244275"}],"container-title":["Informatik-Fachberichte","GWAI-91 15. Fachtagung f\u00fcr K\u00fcnstliche Intelligenz"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-02711-0_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T14:29:49Z","timestamp":1557757789000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-02711-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540545583","9783662027110"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-02711-0_2","relation":{},"ISSN":["0343-3005"],"issn-type":[{"type":"print","value":"0343-3005"}],"subject":[],"published":{"date-parts":[[1991]]}}}