{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:46:00Z","timestamp":1725493560655},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540422877"},{"type":"electronic","value":"9783540482246"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-48224-5_77","type":"book-chapter","created":{"date-parts":[[2007,10,28]],"date-time":"2007-10-28T02:29:04Z","timestamp":1193538544000},"page":"951-962","source":"Crossref","is-referenced-by-count":3,"title":["On the Completeness of Arbitrary Selection Strategies for Paramodulation"],"prefix":"10.1007","author":[{"given":"Miquel","family":"Bofill","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guillem","family":"Godoy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,7,4]]},"reference":[{"issue":"2","key":"77_CR1","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1145\/174652.174655","volume":"41","author":"L. Bachmair","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":"77_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, 1986."},{"issue":"3","key":"77_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":"77_CR4","doi-asserted-by":"crossref","unstructured":"David Basin and Harald Ganzinger. Complexity Analysis Based on Ordered Resolution. In Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS), pages 456\u2013465, New Brunswick, New Jersey, USA, 1996.","DOI":"10.1109\/LICS.1996.561462"},{"issue":"2","key":"77_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 paramodulation. Information and Computation, 121(2):172\u2013192, 1995.","journal-title":"Information and Computation"},{"key":"77_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, 1999.","DOI":"10.1109\/LICS.1999.782618"},{"key":"77_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/3-540-54233-7_140","volume-title":"Proceedings of the Eighteenth International Colloquium on Automata, Languages and Programming (ICALP)","author":"N. Dershowitz","year":"1991","unstructured":"Nachum Dershowitz. Canonical sets of Horn clauses. In J. Leach Albert, B. Monien, and M. Rodr\u00f3guez Artalejo, editors, Proceedings of the Eighteenth International Colloquium on Automata, Languages and Programming (ICALP), LNCS 510, pages 267\u2013278, Madrid, Spain, 1991. Springer-Verlag."},{"key":"77_CR8","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."},{"key":"77_CR9","doi-asserted-by":"crossref","unstructured":"Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings. Comm. of ACM, 22(8), 1979.","DOI":"10.1145\/359138.359142"},{"key":"77_CR10","unstructured":"Hans de Nivelle. Ordering refinements of resolution. Dissertation, Technische Universiteit Delft, Delft, 1996."},{"issue":"3","key":"77_CR11","doi-asserted-by":"publisher","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":"3","key":"77_CR12","first-page":"9","volume":"4","author":"C. Kirchner","year":"1990","unstructured":"Claude Kirchner, H\u00e9l\u00e8ne Kirchner, and Micha\u0451l Rusinowitch. Deduction with symbolic constraints. Revue Fran\u00e7aise d\u2019Intelligence Artificielle, 4(3):9\u201352, 1990.","journal-title":"Revue Fran\u00e7aise d\u2019Intelligence Artificielle"},{"issue":"1","key":"77_CR13","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1006\/jsco.1996.0075","volume":"23","author":"C. Lynch","year":"1997","unstructured":"C. Lynch. Oriented equational logic programming is complete. Journal of Symbolic Computation, 23(1):23\u201346, January 1997.","journal-title":"Journal of Symbolic Computation"},{"key":"77_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1998.2730","volume":"147","author":"R. Nieuwenhuis","year":"1998","unstructured":"Robert Nieuwenhuis. Decidability and complexity analysis by basic paramodulation. Information and Computation, 147:1\u201321, 1998.","journal-title":"Information and Computation"},{"issue":"4","key":"77_CR15","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1006\/jsco.1995.1020","volume":"19","author":"R. 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":"77_CR16","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(to appear), 2001.","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"issue":"2","key":"77_CR17","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1023\/A:1005812220011","volume":"18","author":"C. Weidenbach","year":"1997","unstructured":"Christoph Weidenbach. SPASS\u2014version 0.49. Journal of Automated Reasoning, 18(2):247\u2013252, April 1997.","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48224-5_77","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T22:28:39Z","timestamp":1556922519000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48224-5_77"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540422877","9783540482246"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-48224-5_77","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}