{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:29:03Z","timestamp":1725488943578},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439318"},{"type":"electronic","value":"9783540456209"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45620-1_36","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T03:18:26Z","timestamp":1186888706000},"page":"456-470","source":"Crossref","is-referenced-by-count":3,"title":["Well-Foundedness Is Sufficient for Completeness of Ordered Paramodulation"],"prefix":"10.1007","author":[{"given":"Miquel","family":"Bofill","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Albert","family":"Rubio","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"issue":"2","key":"36_CR1","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1145\/174652.174655","volume":"41","author":"Leo Bachmair and Nachum Dershowitz","year":"1994","unstructured":"Leo Bachmair and Nachum Dershowitz. Equational inference, canonical proofs, and proof orderings. J. of the Association for Computing Machinery, 41(2):236\u2013276, February 1994.","journal-title":"J. of the Association for Computing Machinery"},{"key":"36_CR2","unstructured":"Leo Bachmair, Nachum Dershowitz, and Jieh Hsiang. Orderings for equational proofs. In First IEEE Symposium on Logic in Computer Science (LICS), pages 346\u2013357, Cambridge, Massachusetts, USA, June 16\u201318, 1986. IEEE Computer Society Press."},{"issue":"3","key":"36_CR3","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"Leo Bachmair and Harald Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217\u2013247, 1994.","journal-title":"Journal of Logic and Computation"},{"key":"36_CR4","unstructured":"Leo Bachmair and Harald Ganzinger. Equational reasoning in saturation-based theorem proving. In W. Bibel and P. Schmitt, editors, Automated Deduction: A Basis for Applications. Kluwer, 1998."},{"issue":"2","key":"36_CR5","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1006\/inco.1995.1131","volume":"121","author":"L. Bachmair","year":"1995","unstructured":"L. Bachmair, H. Ganzinger, Chr. Lynch, and W. Snyder. Basic paramod-ulation. Information and Computation, 121(2):172\u2013192, 1995.","journal-title":"Information and Computation"},{"key":"36_CR6","doi-asserted-by":"crossref","unstructured":"Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, and Albert Rubio. Paramodulation with non-monotonic orderings. In 14th IEEE Symposium on Logic in Computer Science (LICS), pages 225\u2013233, Trento, Italy, July 2\u20135, 1999.","DOI":"10.1109\/LICS.1999.782618"},{"key":"36_CR7","doi-asserted-by":"crossref","unstructured":"Miquel Bofill and Albert Rubio. Well-foundedness is sufficient for completeness of Ordered Paramodulation. Long version, 2002. Available at http:\/\/www.lsi.upc.es\/~albert\/papers.html .","DOI":"10.1007\/3-540-45620-1_36"},{"key":"36_CR8","series-title":"Formal Models and Semantics","first-page":"244","volume-title":"Handbook of Theoretical Computer Science","author":"N. Dershowitz","year":"1990","unstructured":"Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, chapter 6, pages 244\u2013320. Elsevier Science Publishers B.V., Amsterdam, New York, Oxford, Tokyo, 1990."},{"issue":"3","key":"36_CR9","doi-asserted-by":"crossref","first-page":"559","DOI":"10.1145\/116825.116833","volume":"38","author":"J. Hsiang","year":"1991","unstructured":"J. Hsiang and M Rusinowitch. Proving refutational completeness of theorem proving strategies: the transfinite semantic tree method. Journal of the ACM, 38(3):559\u2013587, July 1991.","journal-title":"Journal of the ACM"},{"issue":"4","key":"36_CR10","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1006\/jsco.1995.1020","volume":"19","author":"Robert Nieuwenhuis","year":"1995","unstructured":"Robert Nieuwenhuis and Albert Rubio. Theorem Proving with Ordering and Equality Constrained Clauses. Journal of Symbolic Computation, 19(4):321\u2013351, April 1995.","journal-title":"Journal of Symbolic Computation"},{"key":"36_CR11","doi-asserted-by":"crossref","unstructured":"Robert Nieuwenhuis and Albert Rubio. Paramodulation-based theorem proving. In J.A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning. Elsevier Science Publishers and MIT Press, 2001.","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"36_CR12","series-title":"EATCS Monographs on Theoretical Computer Science","volume-title":"Universal Algebra for Computer Scientists","author":"W. Wechler","year":"1991","unstructured":"W. Wechler. Universal Algebra for Computer Scientists, volume 25 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, Berlin, 1991."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-18"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45620-1_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T19:56:04Z","timestamp":1556740564000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45620-1_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439318","9783540456209"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-45620-1_36","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}