{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:48:10Z","timestamp":1749124090854},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540614647"},{"type":"electronic","value":"9783540685968"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61464-8_73","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:40:49Z","timestamp":1330292449000},"page":"428-431","source":"Crossref","is-referenced-by-count":3,"title":["SPIKE-AC: A system for proofs by induction in Associative-Commutative theories"],"prefix":"10.1007","author":[{"given":"Narjes","family":"Berregeb","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adel","family":"Bouhoula","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Micha\u00ebl","family":"Rusinowitch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"36_CR1","volume-title":"PhD thesis","author":"M. Allemand","year":"1995","unstructured":"M. Allemand. Mod\u00e9lisation fonctionnelle et Preuve de circuits avec LP. PhD thesis, Universit\u00e9 de Provence (Aix-Marseille I), 1995."},{"key":"36_CR2","first-page":"329","volume":"1","author":"L. Bachmair","year":"1985","unstructured":"L. Bachmair and D. A. Plaisted. Termination orderings for associative-commutative rewriting systems. Journal of Logic and Computation, 1:329\u2013349, 1985.","journal-title":"Journal of Logic and Computation"},{"key":"36_CR3","doi-asserted-by":"crossref","unstructured":"N. Berregeb, A. Bouhoula, and M. Rusinowitch. Automated verification by induction with associative-commutative operators. To appear in Proceedings of the International Conference on Computer Aided Verification, 1996.","DOI":"10.1007\/3-540-61474-5_71"},{"issue":"2","key":"36_CR4","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/BF00881856","volume":"14","author":"A. Bouhoula","year":"1995","unstructured":"A. Bouhoula and M. Rusinowitch. Implicit induction in conditional theories. Journal of Automated Reasoning, 14(2): 189\u2013235, 1995.","journal-title":"Journal of Automated Reasoning"},{"key":"36_CR5","unstructured":"R. S. Boyer and J. S. Moore. A computational Logic Handbook. 1988."},{"key":"36_CR6","doi-asserted-by":"crossref","unstructured":"R. B\u00fcndgen, W. K\u00fcchlin. Computing ground reducibility and inductively complete positions. In N. Dershowitz, editor, Rewriting Techniques and Applications, LNCS 355, pages 59\u201375, 1989.","DOI":"10.1007\/3-540-51081-8_100"},{"key":"36_CR7","unstructured":"Steven Eker. Improving the efficiency of AC matching and unification. Research report 2104, INRIA, Inria Lorraine & Crin, November 1993."},{"key":"36_CR8","doi-asserted-by":"crossref","unstructured":"S. J. Garland and J. V. Guttag. An overview of LP, the Larch Prover. In N. Dershowitz, editor, Rewriting Techniques and Applications, LNCS 355, pages 137\u2013151, 1989.","DOI":"10.1007\/3-540-51081-8_105"},{"key":"36_CR9","doi-asserted-by":"publisher","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\u201333, 1989.","journal-title":"Information and Computation"},{"key":"36_CR10","doi-asserted-by":"crossref","unstructured":"D. Kapur and P. Narendran. Double-exponential complexity of computing a complete set of AC-unifiers. In IEEE Symposium on Logic in Computer Science, 1992.","DOI":"10.1109\/LICS.1992.185515"},{"key":"36_CR11","doi-asserted-by":"crossref","unstructured":"P. Lescanne. Orme, an implementation of completion procedures as sets of transitions rules. In M. Stickel, editor, International Conference on Automated Deduction, pages 661\u2013662, 1990.","DOI":"10.1007\/3-540-52885-7_130"},{"key":"36_CR12","doi-asserted-by":"crossref","unstructured":"S. Owre, J.M. Rushby, and N. Shankar. A prototype verification system. In D. Kapur, editor, International Conference on Automated Deduction, LNAI 607, pages 748\u2013752, 1992.","DOI":"10.1007\/3-540-55602-8_217"},{"key":"36_CR13","unstructured":"L. Pierre. The formal proof of sequential circuits described in CASCADE using the Boyer-Moore theorem prover. In L. Claesen, editor, Formal VLSI Correctness Verification, 1990."}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61464-8_73.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:32:12Z","timestamp":1619573532000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61464-8_73"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614647","9783540685968"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-61464-8_73","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}