{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:22:13Z","timestamp":1725495733569},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540643012"},{"type":"electronic","value":"9783540697213"}],"license":[{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0052366","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T01:31:11Z","timestamp":1149643871000},"page":"136-137","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["About proofs by consistency"],"prefix":"10.1007","author":[{"given":"Hubert","family":"Comon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,18]]},"reference":[{"key":"11_CR1","unstructured":"L. Bachmair. Proof by consistency in equational theories. In Proc. 3rd IEEE Symp. Logic in Computer Science, Edinburgh, July 1988."},{"key":"11_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-7118-2","volume-title":"Canonical Equational Proofs","author":"L. Bachmair","year":"1991","unstructured":"L. Bachmair. Canonical Equational Proofs. Birkh\u00e4user, Boston, 1991."},{"key":"11_CR3","volume-title":"5th International Conference on Rewriting Techniques and Applications, volume 690 of Lecture Notes in Computer Science","author":"A.-C. Caron","year":"1993","unstructured":"A.-C. Caron, J.-L. Coquid\u00e9, and M. Dauchet. Encompassment properties and automata with constraints. In C. Kirchner, editor, 5th International Conference on Rewriting Techniques and Applications, volume 690 of Lecture Notes in Computer Science, Montreal, Canada, June 1993. Springer-Verlag."},{"key":"11_CR4","volume-title":"Proc. IEEE Symp. on Logic in Computer Science","author":"H. Comon","year":"1997","unstructured":"H. Comon and F. Jacquemard. Ground reducibility is exptime-complete. In Proc. IEEE Symp. on Logic in Computer Science, Varsaw, June 1997. IEEE Comp. Soc. Press."},{"key":"11_CR5","first-page":"259","volume-title":"Proc. 7th Int. Conf. on Automated Deduction, volume 170 of Lecture Notes in Computer Science","author":"L. Pribourg","year":"1984","unstructured":"L. Pribourg. A narrowing procedure for theories with constructors. In R. Shostak, editor, Proc. 7th Int. Conf. on Automated Deduction, volume 170 of Lecture Notes in Computer Science, pages 259\u2013281, Napa, CA., 1984. Springer-Verlag."},{"key":"11_CR6","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/S0747-7171(89)80069-0","volume":"8","author":"L. Fribourg","year":"1989","unstructured":"L. Fribourg. A strong restriction of the inductive completion procedure. Journal of Symbolic Computation, 8:253\u2013276, 1989.","journal-title":"Journal of Symbolic Computation"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"J. A. Goguen. How to prove inductive hypothesis without induction. In Proc. 5th Conf. on Automated Deduction, Les Arcs, France, LNCS 87, July 1980.","DOI":"10.1007\/3-540-10009-1_27"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"G. Huet and J.-M. Hullot. Proofs by induction in equational theories with constructors. J. Comput. Syst. Sci., 25(2), 1982.","DOI":"10.1016\/0022-0000(82)90006-X"},{"key":"11_CR9","volume-title":"Twelfth Annual IEEE Symposium on Logic in Computer Science","author":"J.-P. Jouannaud","year":"1997","unstructured":"J.-P. Jouannaud and A. Bouhoula. Automata-driven automated induction. In Twelfth Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 1997. IEEE Comp. Soc. Press."},{"key":"11_CR10","unstructured":"J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in equational theories without constructors. In Proc. 1st IEEE Symp. Logic in Computer Science, Cambridge, Mass., June 1986."},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82(1), July 1989.","DOI":"10.1016\/0890-5401(89)90062-X"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"D. Kapur and D. Musser. Proof by consistency. Artificial Intelligence, 31(2), Feb. 1987.","DOI":"10.1016\/0004-3702(87)90017-8"},{"key":"11_CR13","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/BF01893885","volume":"28","author":"D. Kapur","year":"1991","unstructured":"D. Kapur, P. Narendran, D. Rosenkrantz, and H. Zhang. Sufficient completeness, ground reducibility and their complexity. Acta Inf., 28:311\u2013350, 1991.","journal-title":"Acta Inf."},{"issue":"4","key":"11_CR14","doi-asserted-by":"publisher","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 Inf., 24(4):395\u2013415, 1987.","journal-title":"Acta Inf."},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"D. Kapur and H. Zhang. An overview of the rewrite rule laboratory. Journal of Mathematics of Computation, 1995.","DOI":"10.1016\/0898-1221(94)00218-A"},{"key":"11_CR16","unstructured":"W. K\u00fcchlin. Inductive completion by ground proof transformation. In H. Ait-Kaci and M. Nivat, editors, Proc. Coll. on the Resolution of Equations in Algebraic Structures, Lakeway. Academic Press, May 1987."},{"issue":"1","key":"11_CR17","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0304-3975(92)90279-O","volume":"106","author":"E. Kounalis","year":"1992","unstructured":"E. Kounalis. Testing for the ground (co)-reducibility in term rewriting systems. Theoretical Computer Science, 106(1):87\u2013117, 1992.","journal-title":"Theoretical Computer Science"},{"key":"11_CR18","unstructured":"D. S. Lankford. A simple explanation of inductionless induction. Technical Report MTP-14, Mathematics Department, Louisiana Tech. Univ., 1981."},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"D. Musser. Proving inductive properties of abstract data types. In Proc. 7th ACM Symp. on Principles of Programming Languages, Las Vegas, 1980.","DOI":"10.1145\/567446.567461"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"U. Reddy. Term rewriting induction. In Proc. 10th Int. Conf. on Automated Deduction, Kaiserslautern, LNCS 449, 1990.","DOI":"10.1007\/3-540-52885-7_86"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0052366","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T13:17:06Z","timestamp":1578489426000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0052366"}},"subtitle":["Abstract"],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540643012","9783540697213"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/bfb0052366","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]},"assertion":[{"value":"18 May 2006","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}