{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:16:43Z","timestamp":1725664603285},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540629504"},{"type":"electronic","value":"9783540690511"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-62950-5_60","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:58:29Z","timestamp":1330279109000},"page":"38-52","source":"Crossref","is-referenced-by-count":4,"title":["Conditional equational specifications of data types with partial operations for inductive theorem proving"],"prefix":"10.1007","author":[{"given":"Ulrich","family":"K\u00fchler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claus-Peter","family":"Wirth","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"4_CR1","unstructured":"J. Avenhaus and K. Madlener. Theorem proving in hierarchical clausal specifications. SEKI-Report SR-95-14, FB Informatik, Universit\u00e4t Kaiserslautern, 1995."},{"key":"4_CR2","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/0022-0000(86)90033-4","volume":"32","author":"J. A. Bergstra","year":"1986","unstructured":"J. A. Bergstra and J. W. Klop. Conditional rewrite rules: Confluence and termination. J. Computer and System Sci., 32:323\u2013362, 1986.","journal-title":"J. Computer and System Sci."},{"key":"4_CR3","doi-asserted-by":"crossref","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. J. Automated Reasoning, 14:189\u2013235, 1995.","journal-title":"J. Automated Reasoning"},{"key":"4_CR4","unstructured":"R. Boyer and J Moore. A Computational Logic. Academic Press, 1979."},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In Handbook of Theoretical Computer Science, pages 243\u2013320. Elsevier Science Publishers B. V., 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"N. Dershowitz, M. Okada, and G. Sivakumar. Confluence of conditional rewrite systems. In 1st CTRS, volume 308 of LNCS, pages 31\u201344. Springer, 1988.","DOI":"10.1007\/3-540-19242-5_3"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification. Springer, 1985.","DOI":"10.1007\/978-3-642-69962-7"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"D. Hutter and C. Sengler. INKA: The next generation. In 13th CADE, volume 1104 of LNAI, pages 288\u2013292. Springer, 1996.","DOI":"10.1007\/3-540-61511-3_92"},{"key":"4_CR9","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/BF00244459","volume":"16","author":"D. Kapur","year":"1996","unstructured":"D. Kapur and M. Subramaniam. New uses of linear arithmetic in automated theorem proving by induction. J. Automated Reasoning, 16:39\u201378, 1996.","journal-title":"J. Automated Reasoning"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"U. K\u00fchler and C.-P. Wirth. Conditional equational specifications of data types with partial operations for inductive theorem proving. SEKI-Report SR-96-11, FB Informatik, Universit\u00e4t Kaiserslautern, 1996.","DOI":"10.1007\/3-540-62950-5_60"},{"key":"4_CR11","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1016\/S0019-9958(85)80005-X","volume":"65","author":"D. A. Plaisted","year":"1985","unstructured":"D. A. Plaisted. Semantic confluence tests and completion methods. Information and Control, 65:182\u2013215, 1985.","journal-title":"Information and Control"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"M. Wirsing. Algebraic specification. In Handbook of Theoretical Computer Science, pages 675\u2013788. Elsevier Science Publishers B. V., 1990.","DOI":"10.1016\/B978-0-444-88074-1.50018-4"},{"key":"4_CR13","unstructured":"C.-P. Wirth. Syntactic confluence criteria for positive\/negative-conditional term rewriting systems. SEKI-Report SR-95-09, FB Informatik, Universit\u00e4t Kaiserslautern, 1995."},{"key":"4_CR14","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1006\/jsco.1994.1004","volume":"17","author":"C.-P. Wirth","year":"1994","unstructured":"C.-P. Wirth and B. Gramlich, A constructor-based approach to positive\/negative-conditional equational specifications. J. Symbolic Computation, 17:51\u201390, 1994.","journal-title":"J. Symbolic Computation"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"C.-P. Wirth and B. Gramlich. On notions of inductive validity for first-order equational clauses. In 12th CADE, volume 814 of LNAI, pages 162\u2013176. Springer, 1994.","DOI":"10.1007\/3-540-58156-1_12"},{"key":"4_CR16","unstructured":"C.-P. Wirth and U. K\u00fchler. Inductive theorem proving in theories specified by positive\/negative-conditional equations. SEKI-Report SR-95-15, FB Informatik, Universit\u00e4t Kaiserslautern, 1995."}],"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-62950-5_60.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:15:04Z","timestamp":1605629704000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-62950-5_60"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540629504","9783540690511"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-62950-5_60","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}