{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:58:26Z","timestamp":1725663506075},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540543176"},{"type":"electronic","value":"9783540475583"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-54317-1_91","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T22:39:49Z","timestamp":1330209589000},"page":"194-205","source":"Crossref","is-referenced-by-count":6,"title":["Proof by consistency in conditional equational theories"],"prefix":"10.1007","author":[{"given":"Eddy","family":"Bevers","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Johan","family":"Lewi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"15_CR1","unstructured":"Ackermann, W. (1962). Solvable cases of the decision problem. North-Holland."},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Bachmair, L. (1988). Proof by Consistency in Equational Theories. Logic in Computer Science, Edinburgh 1988.","DOI":"10.1109\/LICS.1988.5122"},{"key":"15_CR3","volume-title":"Completion of first-order clauses with equality by strict superposition","author":"L. Bachmair","year":"1990","unstructured":"Bachmair, L., Ganzinger, H. (1990). Completion of first-order clauses with equality by strict superposition. 2nd CTRS, Logic and Formal Method Lab, Dept. of Computer Science, Concordia University, Montreal.","edition":"2nd CTRS"},{"key":"15_CR4","volume-title":"Conditional rewrite rules: Confluence and termination. Report IW198\/82","author":"J. Bergstra","year":"1982","unstructured":"Bergstra, J., Klop, J.W. (1982). Conditional rewrite rules: Confluence and termination. Report IW198\/82, Mathematisch Centrum, Amsterdam."},{"key":"15_CR5","unstructured":"Bevers, E., Lewi, J. (1990). Proof by Consistency in Conditional Equational Theories. Report CW 102, Department of Computer Science, K.U.Leuven."},{"key":"15_CR6","first-page":"15","volume":"308","author":"W. Bousdira","year":"1987","unstructured":"Bousdira, W., R\u00e9my, J.L. (1987). Hierarchical contextual rewriting with several levels. Proc. 1st CTRS, LNCS 308, 15\u201330.","journal-title":"LNCS"},{"issue":"3","key":"15_CR7","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"Dershowitz, N. (1982). Orderings for term-rewriting systems. J. Theoretical Computer Science, Vol 17, No 3, 279\u2013301.","journal-title":"J. Theoretical Computer Science"},{"key":"15_CR8","first-page":"31","volume":"308","author":"N. Dershowitz","year":"1987","unstructured":"Dershowitz, N., Okada, M., Sivakumar, G. (1987). Confluence of Conditional Rewrite Systems. 1st CTRS, LNCS 308, 31\u201344.","journal-title":"LNCS"},{"key":"15_CR9","first-page":"538","volume":"310","author":"N. Dershowitz","year":"1988","unstructured":"Dershowitz, N., Okada, M., Sivakumar, G. (1988). Canonical Conditional Rewrite Systems. Proc. 9th CADE, LNCS 310, 538\u2013549.","journal-title":"LNCS"},{"key":"15_CR10","volume-title":"A Maximal-Literal Unit Strategy for Horn Clauses","author":"N. Dershowitz","year":"1990","unstructured":"Dershowitz, N. (1990). A Maximal-Literal Unit Strategy for Horn Clauses. 2nd CTRS, Logie and Formal Method Lab, Dept. of Computer Science, Concordia University, Montreal.","edition":"2nd CTRS"},{"key":"15_CR11","first-page":"105","volume":"226","author":"L. Fribourg","year":"1986","unstructured":"Fribourg, L. (1986). A strong restriction of the inductive completion procedure. ICALP '86, LNCS 226, 105\u2013115.","journal-title":"LNCS"},{"key":"15_CR12","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/S0747-7171(89)80069-0","volume":"8","author":"L. Fribourg","year":"1989","unstructured":"Fribourg, L. (1989). A strong restriction of the inductive completion procedure. Journal of Symbolic Computation, 8, 253\u2013276.","journal-title":"Journal of Symbolic Computation"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Ganzinger, H. (1987a). Ground term confluence in parametric conditional equational specifications. Proc. STACS 1987, LNCS 247.","DOI":"10.1007\/BFb0039613"},{"key":"15_CR14","first-page":"62","volume":"308","author":"H. Ganzinger","year":"1987","unstructured":"Ganzinger, H. (1987b). A Completion Procedure for Conditional Equations. 1st CTRS, LNCS 308, 62\u201383.","journal-title":"LNCS"},{"key":"15_CR15","first-page":"156","volume":"256","author":"R. G\u00f6bel","year":"1987","unstructured":"G\u00f6bel, R. (1987). Ground Confluence. Proc. Rewriting Techniques and Applications, Bordeaux, LNCS 256, 156\u2013167.","journal-title":"LNCS"},{"key":"15_CR16","first-page":"356","volume":"87","author":"J.A. Goguen","year":"1980","unstructured":"Goguen, J.A., (1980). How to Prove Algebraic Inductive Hypotheses Without Induction, with Applications to the Correctness of Data Type Implementation, Proc. 5th CADE, LNCS 87, 356\u2013373","journal-title":"LNCS"},{"key":"15_CR17","unstructured":"Gramlich, B. (1989). Inductive Theorem Proving Using Refined Unfailing Completion Techniques. SEKI Report SR-89-14, Universit\u00e4t Kaiserslautern."},{"key":"15_CR18","unstructured":"Hsiang, J., Rusinowitch, M. (1986). On word problems in equational theories. Tech. Rep. 86\/29, SUNY at Stony Brook."},{"key":"15_CR19","first-page":"349","volume-title":"Equations and rewrite rules: A survey. Formal Language Theory: Perspectives and Open Problems","author":"G. Huet","year":"1980","unstructured":"Huet, G., Oppen, D. (1980). Equations and rewrite rules: A survey. Formal Language Theory: Perspectives and Open Problems, Academic Press, New York, 1980, 349\u2013405."},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Huet, G., Hullot, J. M. (1982). Proofs by induction in equational theories with constructors. 21st IEEE symposium on Foundations of Computer Science, 96\u2013107.","DOI":"10.1016\/0022-0000(82)90006-X"},{"key":"15_CR21","unstructured":"Jouannaud, J.P., Kounalis, E. (1985). Proofs by induction in equational theories without constructors. CRIN 85-R-042, Nancy."},{"key":"15_CR22","unstructured":"Jouannaud, J.P., Waldmann, B. (1986). Reductive Conditional term rewriting systems. Proc. 3rd IFIP Working Conference on Formal Description of Programming Concepts, Ebberup, Denmark, Aug. 1986, North-Holland."},{"key":"15_CR23","volume-title":"Two Generalisations of the Recursive Path Ordering","author":"S. Kamin","year":"1980","unstructured":"Kamin, S., Levy, J.-J. (1980). Two Generalisations of the Recursive Path Ordering, Unpublished note, Dept. of Computer Science, University of Illinois, USA."},{"key":"15_CR24","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1016\/0304-3975(84)90087-2","volume":"33","author":"S. Kaplan","year":"1984","unstructured":"Kaplan, S. (1984). Conditional Rewrite Rules. Journal of Theoretical Computer Science, 33, 175\u2013193.","journal-title":"Journal of Theoretical Computer Science"},{"key":"15_CR25","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/S0747-7171(87)80010-X","volume":"4","author":"S. Kaplan","year":"1987","unstructured":"Kaplan, S. (1987). Simplifying Conditional Term Rewriting Systems: Unification, Termination and Confluence. Journal of Symbolic Computation, 4, 95\u2013334.","journal-title":"Journal of Symbolic Computation"},{"key":"15_CR26","first-page":"99","volume":"230","author":"D. Kapur","year":"1986","unstructured":"Kapur, D., Narendran, P., Zhang, H. (1986). Proof by induction using test sets. Proc. 8th CADE, LNCS 230, Springer New York, 99\u2013117.","journal-title":"LNCS"},{"key":"15_CR27","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0004-3702(87)90017-8","volume":"31","author":"D. Kapur","year":"1987","unstructured":"Kapur, D., Musser, D.R. (1987). Proof by Consistency. Artificial Intelligence, 31, 125\u2013157.","journal-title":"Artificial Intelligence"},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"K\u00fcchlin, W. (1989). Inductive completion by ground proof transformation. Rewriting Techniques, volume 2 of Resolution of Equations in Algebraic Structures, Ait-Kaci, H., Nivat, M. (eds.), Academic Press.","DOI":"10.1016\/B978-0-12-046371-8.50013-4"},{"key":"15_CR29","doi-asserted-by":"crossref","unstructured":"Musser, D. R. (1980). On proving inductive properties of abstract data types. Proceedings 7th Symposium on Principles of Programming Languages, ACM SIGPLAN, 154\u2013162.","DOI":"10.1145\/567446.567461"},{"key":"15_CR30","first-page":"179","volume":"308","author":"M. Okada","year":"1987","unstructured":"Okada, M. (1987). A Logical Analysis on Theory of Conditional Rewriting. 1st CTRS, LNCS 308, 179\u2013196.","journal-title":"LNCS"},{"key":"15_CR31","unstructured":"Paul, E. (1984). Proof by induction in equational theories with relations between constructors. Proceedings 9th Colloquium on trees in Algebra and Programming, Bordeaux, 211\u2013225."},{"key":"15_CR32","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1016\/S0019-9958(85)80005-X","volume":"65","author":"D.A. Plaisted","year":"1985","unstructured":"Plaisted, D.A. (1985). Semantic confluence tests and completion methods. Inf. Control 65:182\u2013215.","journal-title":"Inf. Control"},{"key":"15_CR33","first-page":"46","volume":"202","author":"H. Zhang","year":"1985","unstructured":"Zhang, H., R\u00e9my, J.L. (1985). Contextual rewriting. Rewriting Techniques and Applications, LNCS 202, 46\u201362.","journal-title":"LNCS"}],"container-title":["Lecture Notes in Computer Science","Conditional and Typed Rewriting Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-54317-1_91.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:53:37Z","timestamp":1605646417000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54317-1_91"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540543176","9783540475583"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/3-540-54317-1_91","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}