{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:08:30Z","timestamp":1725484110338},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439295"},{"type":"electronic","value":"9783540456162"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45616-3_13","type":"book-chapter","created":{"date-parts":[[2007,5,17]],"date-time":"2007-05-17T00:26:55Z","timestamp":1179361615000},"page":"176-190","source":"Crossref","is-referenced-by-count":13,"title":["Integration of Equality Reasoning into the Disconnection Calculus"],"prefix":"10.1007","author":[{"given":"Reinhold","family":"Letz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gernot","family":"Stenz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,9]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"L. Bachmair, N. Dershowitz, and D.A. Plaisted. Completion Without Failure. In H. Ait-Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, volume 2, pages 1\u201330. Academic Press, 1989.","DOI":"10.1016\/B978-0-12-046371-8.50007-9"},{"key":"13_CR2","series-title":"Foundations","first-page":"265","volume-title":"Automated Deduction \u2014 A Basis for Applications","author":"B. Beckert","year":"1998","unstructured":"Bernhard Beckert. Rigid E-unification. In Wolfgang Bibel and Peter H. Schmitt, editors, Automated Deduction \u2014 A Basis for Applications, volume I: Foundations, pages 265\u2013289. Kluwer, Dordrecht, 1998."},{"key":"13_CR3","first-page":"353","volume-title":"Automated Deduction: A Basis for Applications. Volume I, Foundations: Calculi and Methods","author":"L. Bachmair","year":"1998","unstructured":"Leo Bachmair and Harald Ganzinger. Equational reasoning in saturation-based theorem proving. In Wolfgang Bibel and Peter H. Schmidt, editors, Automated Deduction: A Basis for Applications. Volume I, Foundations: Calculi and Methods, pages 353\u2013398. Kluwer Academic Publishers, Dordrecht, 1998."},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Jean-Paul Billon. The disconnection method: a confluent integration of unification in the analytic framework. In P. Migliolo, U. Moscato, D. Mundici, and M. Ornaghi, editors, Proceedings of the 5th International Workshop on Theorem Proving with analytic Tableaux and Related Methods (TABLEAUX), volume 1071 of LNAI, pages 110\u2013126, Berlin, May 15\u201317 1996. Springer.","DOI":"10.1007\/3-540-61208-4_8"},{"issue":"4","key":"13_CR5","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1137\/0204036","volume":"4","author":"D. Brand","year":"1975","unstructured":"Daniel Brand. Proving theorems with the modification method. SIAM Journal on Computing, 4(4):412\u2013430, 1975.","journal-title":"SIAM Journal on Computing"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Vincent J. Digricoli and Malcolm C. Harrison. Equality-based binary resolution. Journal of the ACM, 33(2):253\u2013289, April 1986.","DOI":"10.1145\/5383.5389"},{"key":"13_CR7","series-title":"Lect Notes Comput Sci","volume-title":"Proc. International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Copenhagen, Denmark","author":"M. Giese","year":"2002","unstructured":"Martin Giese. A model generation style completeness proof for constraint tableaux with superposition. In Proc. International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Copenhagen, Denmark, LNCS. Springer-Verlag, 2002. To appear."},{"key":"13_CR8","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/0304-3975(89)90004-2","volume":"67","author":"J. H. Gallier","year":"1989","unstructured":"Jean H. Gallier and Wayne Snyder. Complete sets of transformations for general E-unification. Theoretical Computer Science, 67:203\u2013260, 1989.","journal-title":"Theoretical Computer Science"},{"key":"13_CR9","first-page":"695","volume-title":"Proceedings of the 8th International Conference on Logic for Programming and Automated Reasoning (LPAR 2001), Havanna, Cuba","author":"T. Genet","year":"2001","unstructured":"Thomas Genet and Val\u00e9rie Viet Tirem Tong. Reachability Analysis of Term Rewriting Systems with timbuk. In Andrei Voronkov, editor, Proceedings of the 8th International Conference on Logic for Programming and Automated Reasoning (LPAR 2001), Havanna, Cuba, pages 695\u2013706. Springer, Berlin, December 2001."},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"D.E. Knuth and P.B. Bendix. Simple Word Problems in Universal Algebras. In J. Leech, editor, Computational Algebra, pages 263\u2013297. Pergamon Press, 1970.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"13_CR11","volume-title":"Automated theorem proving: A logical basis","author":"D. W. Loveland","year":"1978","unstructured":"Don W. Loveland. Automated theorem proving: A logical basis. North Holland, New York, 1978."},{"key":"13_CR12","series-title":"LNAI","first-page":"381","volume-title":"Proceedings of the International Joint Conference on Automated Reasoning (IJCAR-2001), Siena, Italy","author":"R. Letz","year":"2001","unstructured":"Reinhold Letz and Gernot Stenz. DCTP: A Disconnection Calculus Theorem Prover. In Rajeev Gor\u00e9, Alexander Leitsch, and Tobias Nipkow, editors, Proceedings of the International Joint Conference on Automated Reasoning (IJCAR-2001), Siena, Italy, volume 2083 of LNAI, pages 381\u2013385. Springer, Berlin, June 2001."},{"key":"13_CR13","first-page":"142","volume-title":"Proceedings of the 8th International Conference on Logic for Programming and Automated Reasoning (LPAR 2001), Havanna, Cuba","author":"R. Letz","year":"2001","unstructured":"Reinhold Letz and Gernot Stenz. Proof and Model Generation with Disconnection Tableaux. In Andrei Voronkov, editor, Proceedings of the 8th International Conference on Logic for Programming and Automated Reasoning (LPAR 2001), Havanna, Cuba, pages 142\u2013156. Springer, Berlin, December 2001."},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Max Moser, Ortrun Ibens, Reinhold Letz, Joachim Steinbach, Christoph Goller, Johann Schumann, and Klaus Mayr. SETHEO and E-SETHEO\u2014 The CADE-13 Systems. Journal of Automated Reasoning, 18(2):237\u2013246, April 1997.","DOI":"10.1023\/A:1005808119103"},{"key":"13_CR15","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/BF00244513","volume":"4","author":"F. Oppacher","year":"1988","unstructured":"F. Oppacher and E. Suen. HARP: A tableau-based theorem prover. Journal of Automated Reasoning, 4:69\u2013100, 1988.","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"13_CR16","first-page":"25","volume":"9","author":"D. A. Plaisted","year":"1992","unstructured":"David A. Plaisted and Shie-Jue Lee. Eliminating duplication with the hyper-linking strategy. Journal of Automated Reasoning, 9(1):25\u201342, 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"13_CR17","first-page":"135","volume":"4","author":"G. A. Robinson","year":"1969","unstructured":"G. A. Robinson and L. Wos. Paramodulation and theorem proving in first-order theories with equality. Machine Intelligence, 4:135\u2013150, 1969.","journal-title":"Machine Intelligence"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45616-3_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,11]],"date-time":"2023-05-11T18:04:42Z","timestamp":1683828282000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45616-3_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439295","9783540456162"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-45616-3_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}