{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:03:47Z","timestamp":1725663827060},"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_12","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:21:20Z","timestamp":1330269680000},"page":"162-176","source":"Crossref","is-referenced-by-count":7,"title":["On notions of inductive validity for first-order equational clauses"],"prefix":"10.1007","author":[{"given":"Claus-Peter","family":"Wirth","sequence":"first","affiliation":[]},{"given":"Bernhard","family":"Gramlich","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"12_CR1","unstructured":"J. Avenhaus, K. Becker. Conditional rewriting modulo a built-in algebra. SEKI-Report SR-92-11, FB Informatik, Univ. Kaiserslautern, 1992."},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"L. Bachmair. Proof by consistency in equational theories. In Proc. 3rd IEEE Symposium on Logic in Computer Science, pp. 228\u2013233, 1988.","DOI":"10.1109\/LICS.1988.5122"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"K. Becker. Semantics for positive\/negative conditional rewrite systems. In M. Rusinowitch, J.L. R\u00e9my, eds., Proc. 3rd CTRS, LNCS 656, pp. 213\u2013225. Springer, 1993.","DOI":"10.1007\/3-540-56393-8_16"},{"key":"12_CR4","unstructured":"L. Bachmair, H. Ganzinger. Perfect model semantics for logic programs with equality. In Proc. 8th ICLP, pp. 645\u2013659. MIT Press, 1991."},{"key":"12_CR5","unstructured":"A. Bouhoula, E. Kounalis, M. Rusinowitch. Automated mathematical induction. Rapport de Recherche 1663, INRIA, April 1992."},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"E. Beyers, J. Levi. Proof by consistency in conditional equational theories. In S. Kaplan, M. Okada, eds., Proc. 2nd CTRS, LNCS 516, pp. 194\u2013205. Springer, 1990.","DOI":"10.1007\/3-540-54317-1_91"},{"key":"12_CR7","unstructured":"R. S. Boyer, J S. Moore. A Computational Logic. Academic Press, 1979."},{"key":"12_CR8","unstructured":"A. Bouhoula, M. Rusinowitch. Automatic case analysis in proof by induction. In Proc. 13th IJCAI, pp. 88\u201394, 1993."},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"N. Dershowitz, J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, ed., Formal models and semantics, Handbook of Theoretical Computer Science, vol. B, chapter 6, pp. 243\u2013320. MIT Press, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"N. Dershowitz, M. Okada, G. Sivakumar. Confluence of conditional rewrite systems. In S. Kaplan, J.-P. Jouannaud, eds., Proc. 1st CTRS, LNCS 308, pp. 31\u201344. Springer, 1988.","DOI":"10.1007\/3-540-19242-5_3"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"H. Ganzinger, J. Stuber. Inductive theorem proving by consistency for first-order clauses. In M. Rusinowitch, J.-L. R\u00e9my, eds., Proc. of 3rd CTRS, LNCS 656, pp. 226\u2013241. Springer, 1993.","DOI":"10.1007\/3-540-56393-8_17"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"S. Kaplan. Positive\/negative conditional rewriting. In S. Kaplan, J.-P. Jouannaud, eds., Proc. 1st CTRS, LNCS 308, pp. 129\u2013143. Springer, 1987.","DOI":"10.1007\/3-540-19242-5_11"},{"key":"12_CR13","unstructured":"D. Kapur, D. R. Musser. Inductive reasoning with incomplete specifications. Prelim. report. In Proc. 1st LICS, Cambridge, MA, 1986."},{"key":"12_CR14","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0004-3702(87)90017-8","volume":"31","author":"D. Kapur","year":"1987","unstructured":"D. Kapur, D. R. Musser. Proof by consistency. Artificial Intelligence, 31:125\u2013157, 1987.","journal-title":"Artificial Intelligence"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"E. Kounalis, M. Rusinowitch. On word problems in Horn theories. In E. Lusk, R. Overbeek, eds., Proc. 9th CADE, LNCS 310, pp. 527\u2013535. Springer, 1988.","DOI":"10.1007\/BFb0012854"},{"key":"12_CR16","unstructured":"E. Kounalis, M. Rusinowitch. Mechanizing inductive reasoning. In Proc. 8th AAAI, pp. 240\u2013245. MIT Press, 1990."},{"key":"12_CR17","unstructured":"P. Padawitz. Horn logic and rewriting for functional and logic program design. Technical Report MIP-9002, Univ. Passau, 1990."},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"G. Smolka, W. Nutt, J.A. Goguen, J. Meseguer. Order-sorted equational computation. In H. Ait-Kaci, M. Nivat, eds., Proc. CREAS, vol. 2, Academic Press, 1989.","DOI":"10.1016\/B978-0-12-046371-8.50016-X"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"C. Walther. Mathematical induction. In Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 2, Clarendon Press, 1994.","DOI":"10.1093\/oso\/9780198537465.003.0003"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"C.-P. Wirth, B. Gramlich. A constructor-based approach for positive\/negative-conditional equational specifications. In M. Rusinowitch, J.-L. R\u00e9my, eds., Proc. of 3rd CTRS, LNCS 656, pp. 198\u2013212. Springer, 1993. Revised and extended version to appear in J. Symbolic Computation.","DOI":"10.1007\/3-540-56393-8_15"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"C.-P. Wirth, B. Gramlich, U. K\u00fchler, H. Prote. Constructor-based inductive validity in positive\/negative-conditional equational specifications. SEKI-Report SR-93-05, FB Informatik, Univ. Kaiserslautern, 1993.","DOI":"10.1007\/3-540-56393-8_15"},{"key":"12_CR22","volume-title":"PhD thesis","author":"H. Zhang","year":"1988","unstructured":"H. Zhang. Reduction, Superposition and Induction: Automated Reasoning in an Equational Logic. PhD thesis, Rensselaer Polytech. Inst., Troy, NY, 1988."},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"H. Zhang, D. Kapur, M.S. Krishnamoorthy. A mechanizable induction principle for equational specifications. In E. Lusk, R. Overbeek, eds., Proc. 9th CADE, LNCS 310, pp. 162\u2013181. Springer, 1988.","DOI":"10.1007\/BFb0012831"}],"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_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T15:48:16Z","timestamp":1713628096000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58156-1_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581567","9783540484677"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-58156-1_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}