{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:03:22Z","timestamp":1725663802636},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540545071"},{"type":"electronic","value":"9783540384205"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-54507-7_13","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T17:56:21Z","timestamp":1330192581000},"page":"156-169","source":"Crossref","is-referenced-by-count":1,"title":["Building in equational theories into the connection method"],"prefix":"10.1007","author":[{"given":"Uwe","family":"Petermann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"13_CR1","first-page":"653","volume-title":"Proc. AFIP 70, Spring Joint Comp. Conf.","author":"R. Anderson","year":"1970","unstructured":"Anderson R., Completeness results for E-resolution, In Proc. AFIP 70, Spring Joint Comp. Conf., AFIPS Press, Reston VA, pp 653\u2013656, 1970."},{"key":"13_CR2","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P. Andrews","year":"1981","unstructured":"Andrews P., Theorem proving via general matings, J.ACM, 28, 193\u2013214, 1981.","journal-title":"J.ACM"},{"volume-title":"Deduction systems","year":"1987","key":"13_CR3","unstructured":"K. H. Blaesius, H. J. Buerckert (Eds.), Deduction systems (in german), Oldenbourg-Verlag, Muenchen, Wien, 1987."},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Bachmair L., Ganzinger H., On restrictions of ordered paramodulation with simplification, Proc. CADE 1990, pp. 427\u2013441, 1990.","DOI":"10.1007\/3-540-52885-7_105"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Bibel W., Automated theorem proving, Verlag Vieweg, 1982, 2 nd ed. 1987.","DOI":"10.1007\/978-3-322-90100-2"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Debart F., Enjalbert P., Lescot M., Multi modal logic programming using equational and order-sorted logic, Report, Lab. d'Informatique, Univ. de Caen, 1990.","DOI":"10.1007\/3-540-53162-9_30"},{"issue":"2","key":"13_CR7","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1145\/5383.5389","volume":"33","author":"V. J. Digricoli","year":"1986","unstructured":"Digricoli V. J., Harrison M. C., Equality-based binary resolution, J. ACM, Vol. 33, Nr. 2, April 1986, pp. 253\u2013289.","journal-title":"J. ACM"},{"key":"13_CR8","unstructured":"Jouannaud J. P., Kirchner C., Solving equations in abstract algebras: a rule-based survey of unification, Report 561\/1990, L.R.I., Univ. de Paris-Sud, 1990."},{"key":"13_CR9","unstructured":"Morris J. B., E-resolution: An extension of resolution to include the equality relation, In Proc. IJCAI 1969 (Washington D.C.), Walker D.E., Norton L.M., Eds., pp. 287\u2013294, 1969."},{"key":"13_CR10","unstructured":"Petermann U., Towards a connection procedure with built in theories, in Proc. JELIA 90, European Workshop on Logic in AI, Amsterdam Sept. 90, LNCS, Springer Publ., 1990."},{"key":"13_CR11","unstructured":"Petermann U., Building in Theories into a first-order proof procedure based on the connection method, Preprint NTZ-Nr. 16\/90, Naturwissenschaftlich \u2014 Theoretisches Zentrum and Department of Informatics, Leipzig University, 1990."},{"key":"13_CR12","unstructured":"Praecklein A., Solving equality reasoning problems with a connection graph theorem prover, SEKI-Report, SR-90-07, FB Informatik, Univ. Kaiserslautern, 1990."},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Reichel H., Initial computability, algebraic specification and partial algbras, Oxford Univ. Press, 1987.","DOI":"10.1515\/9783112573426"},{"key":"13_CR14","unstructured":"Robinson G., Wos L., Paramodulation and theorem proving in first-order theories with equality, Machine Intelligence, 4, 1969."},{"issue":"4","key":"13_CR15","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/BF00244275","volume":"1","author":"M. Stickel","year":"1985","unstructured":"Stickel M., Automated deduction by theory resolution, J. Autom. Reasoning, 1, 4 (1985), 333\u2013356.","journal-title":"J. Autom. Reasoning"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"L.T. Wos, G.A. Robinson, D.F. Carson, L. Shalla, The concept of demodulation in theorem proving, J.ACM, Vol. 14, Nr. 4, Oct. 1967.","DOI":"10.1145\/321420.321429"}],"container-title":["Lecture Notes in Computer Science","Fundamentals of Artificial Intelligence Research"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-54507-7_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T14:10:20Z","timestamp":1687270220000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54507-7_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540545071","9783540384205"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-54507-7_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}