{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:03:46Z","timestamp":1725663826945},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540581567"},{"type":"electronic","value":"9783540484677"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58156-1_10","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:21:40Z","timestamp":1330269700000},"page":"133-147","source":"Crossref","is-referenced-by-count":0,"title":["On the connection between narrowing and proof by consistency"],"prefix":"10.1007","author":[{"given":"Olav","family":"Lysne","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"L. Bachmair. Proof by consistency in equational theories. In Proceedings 3rd IEEE Symposium on Logic in Computer Science, Edinburgh (UK), pages 228\u2013233, 1988.","DOI":"10.1109\/LICS.1988.5122"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"E. Bevers and J. Lewi. Proof by consistency in conditional equational theories. In Proceedings Second International Workshop on Conditional and Typed Rewriting Systems, volume 516 of Lecture Notes in Computer Science, pages 194\u2013205. Springer-Verlag, 1990.","DOI":"10.1007\/3-540-54317-1_91"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"J. Chabin and P. R\u00e9ty. Narrowing directed by a graph of terms. In Proceedings 4th Conference on Rewriting Techniques and Applications, Como (Italy), volume 488 of Lecture Notes in Computer Science, pages 112\u2013123, 1991.","DOI":"10.1007\/3-540-53904-2_90"},{"key":"10_CR4","volume-title":"volume 607 of Lecture Notes in Artificial Intelligence","author":"J. Christian","year":"1992","unstructured":"J. Christian. Some termination criteria for narrowing and E-narrowing. In Proceedings 11th International Conference on Automated Deduction, Saratoga Springs (NY, USA), volume 607 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 1992."},{"key":"10_CR5","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/0304-3975(90)90032-D","volume":"72","author":"R. Echahed","year":"1990","unstructured":"R. Echahed. On completeness of narrowing strategies. Theoretical Computer Science, 72:133\u2013146, 1990.","journal-title":"Theoretical Computer Science"},{"key":"10_CR6","first-page":"259","volume-title":"volume 632 of Lecture Notes in Computer Science","author":"R. Echahed","year":"1992","unstructured":"R. Echahed. Uniform narrowing strategies. In Proceedings 3rd International Conference on Algebraic and Logic Programming, Pisa (Italy), volume 632 of Lecture Notes in Computer Science, pages 259\u2013275. Springer-Verlag, 1992."},{"key":"10_CR7","unstructured":"M. Fay. First-order unification in an equational theory. In Proceedings of the 4th Workshop on Automated Deduction, pages 161\u2013167, 1979."},{"key":"10_CR8","unstructured":"L. Fribourg. SLOG: A logic programming interpreter based on clausal superposition and rewriting. In Proceedings of the 1985 Symposium on Logic Programming, Boston, pages 172\u2013184, 1985."},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"L. Fribourg. A strong restriction on the inductive completion procedure. In Proceedings 13th International Colloquium on Automata, Languages and Programming, volume 226 of Lecture Notes in Computer Science, pages 105\u2013115. Springer-Verlag, 1986.","DOI":"10.1007\/3-540-16761-7_60"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"J. A. Goguen. How to prove inductive hypotheses without induction. In W. Bibel and R. Kowalski, editors, Proceedings of the 5th Conference on Automated Deduction, volume 87 of Lecture Notes in Computer Science, pages 356\u2013373. Springer-Verlag, 1980.","DOI":"10.1007\/3-540-10009-1_27"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"G. Huet and J.-M. Hullot. Proofs by induction in equational theories with constructors. Journal of Computer and System Sciences, pages 239\u2013266, 1982.","DOI":"10.1016\/0022-0000(82)90006-X"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"J.-M. Hullot. Canonical forms and unification. In Proceedings 5th International Conference on Automated Deduction, volume 87, pages 318\u2013334. Springer-Verlag, 1980.","DOI":"10.21236\/ADA087640"},{"issue":"1","key":"10_CR13","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(89)90062-X","volume":"82","author":"J.-P. Jouannaud","year":"1989","unstructured":"J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82(1):1\u201333, July 1989.","journal-title":"Information and Computation"},{"issue":"4","key":"10_CR14","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1007\/BF00292110","volume":"24","author":"D. Kapur","year":"1987","unstructured":"D. Kapur, P. Narendran, and H. Zhang. On sufficient-completeness and related properties of term rewriting systems. Acta Informatica, 24(4):395\u2013415, 1987.","journal-title":"Acta Informatica"},{"key":"10_CR15","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D. E. Knuth","year":"1970","unstructured":"D. E. Knuth and P. B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263\u2013297. Pergamon Press, Oxford, 1970."},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"W. K\u00fcchlin. Inductive completion by ground proof transformation. In H. A\u00cft-Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, volume 2 of Rewriting Techniques, chapter 7. Academic Press, 1989.","DOI":"10.1016\/B978-0-12-046371-8.50013-4"},{"key":"10_CR17","first-page":"276","volume-title":"volume 632 of Lecture Notes in Computer Science","author":"O. Lysne","year":"1992","unstructured":"O. Lysne. Proof by consistency in constructive systems with final algebra semantics. In Proceedings 3rd International Conference on Algebraic and Logic Programming, Pisa (Italy), volume 632 of Lecture Notes in Computer Science, pages 276\u2013290. Springer-Verlag, 1992."},{"key":"10_CR18","unstructured":"J. Meseguer and J. A. Goguen. Initiality, induction and computability. In M. Nivat and J. C. Reynolds, editors, Algebraic Methods in Semantics, chapter 14. Cambridge University Press, 1985."},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"D. L. Musser. On proving inductive properties in abstract data types. In Proceedings of the 7th Annual ACM Symposium on Principles of Programming Languages, pages 154\u2013162, January 1980.","DOI":"10.1145\/567446.567461"},{"key":"10_CR20","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1016\/S0747-7171(89)80014-8","volume":"7","author":"W. Nutt","year":"1989","unstructured":"W. Nutt, P. R\u00e9ty, and G. Smolka. Basic narrowing revisited. Journal of Symbolic Computation, 7:295\u2013317, 1989.","journal-title":"Journal of Symbolic Computation"},{"key":"10_CR21","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1016\/S0019-9958(85)80005-X","volume":"65","author":"D. Plaisted","year":"1985","unstructured":"D. Plaisted. Semantic confluence tests and completion methods. Information and Control, 65:182\u2013215, 1985.","journal-title":"Information and Control"},{"key":"10_CR22","first-page":"228","volume-title":"volume 256 of Lecture Notes in Computer Science","author":"P. R\u00e9ty","year":"1987","unstructured":"P. R\u00e9ty. Improving basic narrowing techniques. In Proceedings 2nd Conference on Rewriting Techniques and Applications, Bordeaux (France), volume 256 of Lecture Notes in Computer Science, pages 228\u2013241. Springer-Verlag, 1987."},{"key":"10_CR23","first-page":"727","volume-title":"volume 317 of Lecture Notes in Computer Science","author":"J. You","year":"1988","unstructured":"Jia-Huai You. Outer narrowing for equational theories based on constructors. In Proceedings 15th International Colloquium on Automata, Languages and Programming, Tampere (Finland), volume 317 of Lecture Notes in Computer Science, pages 727\u2013741. Springer-Verlag, 1988."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-12"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58156-1_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:17:31Z","timestamp":1605647851000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58156-1_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581567","9783540484677"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-58156-1_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}