{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T21:01:08Z","timestamp":1751662868446,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":84,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540250517"},{"type":"electronic","value":"9783540322542"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-32254-2_12","type":"book-chapter","created":{"date-parts":[[2010,6,22]],"date-time":"2010-06-22T19:16:54Z","timestamp":1277234214000},"page":"192-203","source":"Crossref","is-referenced-by-count":5,"title":["History and Future of Implicit and Inductionless Induction: Beware the Old Jade and the Zombie!"],"prefix":"10.1007","author":[{"given":"Claus-Peter","family":"Wirth","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"volume-title":"Resolution of Equations in Algebraic Structures","year":"1989","key":"12_CR1","unstructured":"Ait-Kaci, H., Nivat, M. (eds.): Resolution of Equations in Algebraic Structures. Academic Press, London (1989)"},{"key":"12_CR2","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1006\/jsco.2002.0549","volume":"34","author":"A. Armando","year":"2002","unstructured":"Armando, A., Rusinowitch, M., Stratulat, S.: Incorporating Decision Procedures in Implicit Induction. J. Symbolic Computation\u00a034, 241\u2013258 (2002)","journal-title":"J. Symbolic Computation"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Autexier, S., Hutter, D., Mantel, H., Schairer, A.: Inka 5.0 \u2013 A Logical Voyager. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 207\u2013211. Springer, Heidelberg (1999)","DOI":"10.1007\/3-540-48660-7_15"},{"key":"12_CR4","unstructured":"Avenhaus, J., Madlener, K.: Theorem Proving in Hierarchical Clausal Specifications. SEKI-Report SR\u201395\u201314 (SFB), Univ. Kaiserslautern (1995), http:\/\/www-madlener.informatik.uni-kl.de\/seki\/1995\/Avenhaus.SR-95-14.ps.gz (March 07, 2002)"},{"key":"12_CR5","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/BFb0027405","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"M. Baaz","year":"1997","unstructured":"Baaz, M., Egly, U., Ferm\u00fcller, C.G.: Lean Induction Principles for Tableaus. In: Galmiche, D. (ed.) TABLEAUX 1997. LNCS (LNAI), vol.\u00a01227, pp. 62\u201375. Springer, Heidelberg (1997)"},{"key":"12_CR6","first-page":"228","volume-title":"3 rd IEEE symposium on Logic In Computer Sci.","author":"L. Bachmair","year":"1988","unstructured":"Bachmair, L.: Proof By Consistency in Equational Theories. In: 3 rd IEEE symposium on Logic In Computer Sci., pp. 228\u2013233. IEEE Press, Los Alamitos (1988)"},{"key":"12_CR7","volume-title":"Proof By Consistency","author":"L. Bachmair","year":"1991","unstructured":"Bachmair, L.: Proof By Consistency. Birkhauser, Boston (1991)"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1007\/3-540-56610-4_55","volume-title":"TAPSOFT \u201993: Theory and Practice of Software Development","author":"K. Becker","year":"1993","unstructured":"Becker, K.: Proving Ground Confluence and Inductive Validity in Constructor-Based Equational Specifications. In: Gaudel, M.-C., Jouannaud, J.-P. (eds.) CAAP 1993, FASE 1993, and TAPSOFT 1993. LNCS, vol.\u00a0668, pp. 46\u201360. Springer, Heidelberg (1993)"},{"key":"12_CR9","unstructured":"Becker, K.: Rewrite Operationalization of Clausal Specifications with Predefined Structures. Ph.D. thesis, FB Informatik, Univ. Kaiserslautern (1994)"},{"key":"12_CR10","unstructured":"Becker, K.: How to Prove Ground Confluence. SEKI-Report SR\u201396\u201302, Univ. Kaiserslautern (1996)"},{"key":"12_CR11","first-page":"85","volume":"11","author":"R. Berghammer","year":"1993","unstructured":"Berghammer, R.: On the Characterization of the Integers: The Hidden Function Problem Revisited. Acta Cybernetica\u00a011, 85\u201396 (1993) (szeged)","journal-title":"Acta Cybernetica"},{"key":"#cr-split#-12_CR12.1","doi-asserted-by":"crossref","unstructured":"Bevers, E., Lewi, J.: Proof by Consistency in Conditional Equational Theories. Report CW 102, rev., Dept. Comp. Sci., K. U. Leuven (July 1990);","DOI":"10.1007\/3-540-54317-1_91"},{"key":"#cr-split#-12_CR12.2","unstructured":"Short version In: Okada, M., Kaplan, S. (eds.): CTRS 1990. LNCS, vol.??516, pp.194-205. Springer, Heidelberg (1991)"},{"key":"12_CR13","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/BF00881856","volume":"14","author":"A. Bouhoula","year":"1995","unstructured":"Bouhoula, A., Rusinowitch, M.: Implicit Induction in Conditional Theories. J. Automated Reasoning\u00a014, 189\u2013235 (1995)","journal-title":"J. Automated Reasoning"},{"key":"12_CR14","unstructured":"Bouhoula, A., Kounalis, E., Rusinowitch, M.: Automated Mathematical Induction. Technical Report 1636, INRIA (1992)"},{"key":"12_CR15","volume-title":"A Computational Logic","author":"R.S. Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic. Academic Press, London (1979)"},{"key":"12_CR16","volume-title":"A Computational Logic Handbook","author":"R.S. Boyer","year":"1988","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic Handbook. Academic Press, London (1988)"},{"key":"12_CR17","series-title":"NATO ASI Series","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1007\/978-3-642-74884-4_4","volume-title":"Constructive Methods in Computing Science","author":"R.S. Boyer","year":"1989","unstructured":"Boyer, R.S., Moore, J.S.: The Addition of Bounded Quantification and Partial Functions to A Computational Logic and Its Theorem Prover. In: Broy, M. (ed.) Constructive Methods in Computing Science. NATO ASI Series, vol.\u00a0F 55, pp. 95\u2013145. Springer, Heidelberg (1989)"},{"key":"12_CR18","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/BFb0012826","volume-title":"9th International Conference on Automated Deduction","author":"A. Bundy","year":"1988","unstructured":"Bundy, A.: The Use of Explicit Proof Plans to Guide Inductive Proofs. In: Lusk, E.\u2018., Overbeek, R. (eds.) CADE 1988. LNCS (LNAI), vol.\u00a0310, pp. 111\u2013120. Springer, Heidelberg (1988)"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Comon, H.: Inductionless induction. In: [60], vol.\u00a0I, pp. 913\u2013970 (2001)","DOI":"10.1016\/B978-044450813-3\/50016-3"},{"key":"12_CR20","unstructured":"Comon, H., Nieuwenhuis, R.: Induction = I-Axiomatization + First-order Consistency. Technical Report, ENS Cachan (1998)"},{"key":"12_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1007\/3-540-56393-8_27","volume-title":"Conditional Term Rewriting Systems","author":"U. Fraus","year":"1993","unstructured":"Fraus, U.: A Calculus for Conditional Inductive Theorem Proving. In: Rusinowitch, M., Remy, J.-L. (eds.) CTRS 1992. LNCS, vol.\u00a0656, pp. 357\u2013362. Springer, Heidelberg (1993)"},{"key":"12_CR22","unstructured":"Fraus, U.: Mechanizing Inductive Theorem Proving in Conditional Theories. Ph.D. thesis, Univ. Passau (1994)"},{"key":"12_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/3-540-16761-7_60","volume-title":"Automata, Languages and Programming","author":"L. Fribourg","year":"1986","unstructured":"Fribourg, L.: A Strong Restriction of the Inductive Completion Procedure. In: Kott, L. (ed.) ICALP 1986. LNCS, vol.\u00a0226, pp. 105\u2013116. Springer, Heidelberg (1986); Also in: J. Symbolic Computation 8, 253\u2013276 (1989)"},{"volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming","year":"1993","key":"12_CR24","unstructured":"Gabbay, D.M., Hogger, C.J., Robinson, J.A. (eds.): Handbook of Logic in Artificial Intelligence and Logic Programming. Clarendon Press, Oxford (1993ff.)"},{"key":"#cr-split#-12_CR25.1","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Stuber, J.: Inductive Theorem Proving by Consistency for First-Order Clauses. In: Informatik-Festschrift zum 60. Geburtstag von G??nter Hotz. pp. 441???462. Teubner Verlag, Stuttgart (1992);","DOI":"10.1007\/978-3-322-95233-2_27"},{"key":"#cr-split#-12_CR25.2","unstructured":"Also In: Rusinowitch, M., Remy, J.-L. (eds.): CTRS 1992. LNCS, vol.??656. Springer, Heidelberg (1993)"},{"key":"12_CR26","unstructured":"Gentzen, G.: Die gegenw\u00e4rtige Lage in der mathematischen Grundlagenforschung \u2013 Neue Fassung des Widerspruchsfreiheitsbeweises f\u00fcr die reine Zahlentheorie. Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften, Folge 4, Leipzig (1938)"},{"key":"12_CR27","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/BF01564760","volume":"119","author":"G. Gentzen","year":"1943","unstructured":"Gentzen, G.: Beweisbarkeit und Unbeweisbarkeit von Anfangsf\u00e4llen der transfiniten Induktion in der reinen Zahlentheorie. Mathematische Annalen\u00a0119, 140\u2013161 (1943)","journal-title":"Mathematische Annalen"},{"key":"12_CR28","unstructured":"Geser, A.: A Principle of Non-Wellfounded Induction. In: Margaria, T. (ed.) Kolloquium Programmiersprachen und Grundlagen der Programmierung, MIP\u20139519, pp. 117\u2013124. Univ. Passau. (1995)"},{"key":"12_CR29","unstructured":"Giese, M.: Integriertes automatisches und interaktives Beweisen: die Kalk\u00fclebene. Master\u2019s thesis, Univ. Karlsruhe (1998), http:\/\/i11www.ira.uka.de\/~giese\/da.ps.gz (May 09, 2000)"},{"key":"12_CR30","volume-title":"9th German Workshop on AI, IFB 118","author":"R. G\u00f6bel","year":"1985","unstructured":"G\u00f6bel, R.: Completion of Globally Finite Term Rewriting Systems for Inductive Proofs. In: 9th German Workshop on AI, IFB 118. Springer, Heidelberg (1985)"},{"key":"12_CR31","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/BF01700692","volume":"38","author":"K. G\u00f6del","year":"1931","unstructured":"G\u00f6del, K.: \u00dcber formal unentscheidbare S\u00e4tze der Principia Mathematica und verwandter Systeme I. Monatshefte f\u00fcr Mathematik und Physik\u00a038, 173\u2013198 (1931)","journal-title":"Monatshefte f\u00fcr Mathematik und Physik"},{"key":"12_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1007\/3-540-10009-1_27","volume-title":"5th Conference on Automated Deduction","author":"J. Goguen","year":"1980","unstructured":"Goguen, J.: How to Prove Algebraic Inductive Hypotheses Without Induction. In: Bibel, W. (ed.) CADE 1980. LNCS, vol.\u00a087, pp. 356\u2013373. Springer, Heidelberg (1980)"},{"key":"#cr-split#-12_CR33.1","unstructured":"Gramlich, B.: Inductive Theorem Proving Using Refined Unfailing Completion Techniques. SEKI-Report SR???89???14 (SFB), Univ. Kaiserslautern (1989);"},{"key":"#cr-split#-12_CR33.2","doi-asserted-by":"crossref","unstructured":"Short version In: 9 th ECAI 1990, pp. 314???319. Pitman Publ. (1990)","DOI":"10.1007\/BF02935530"},{"key":"12_CR34","doi-asserted-by":"crossref","unstructured":"Gramlich, B.: Completion Based Inductive Theorem Proving: A Case Study in Verifying Sorting Algorithms. SEKI-Report SR\u201390\u201304, Univ. Kaiserslautern (1990)","DOI":"10.1007\/3-540-52885-7_127"},{"key":"12_CR35","unstructured":"Gramlich, B., Lindner, W.: A Guide to Unicom, an Inductive Theorem Prover Based on Rewriting and Completion Techniques. SEKI-Report SR-91\u201317 (SFB) Univ. Kaiserslautern (1991), http:\/\/agent.informatik.uni-kl.de\/seki\/1991\/Lindner.SR-91-17.ps.gz (May 09, 2000)"},{"key":"#cr-split#-12_CR36.1","doi-asserted-by":"crossref","unstructured":"Huet, G., Hullot, J.-M.: Proofs by Induction in Equational Theories with Constructors. In: 21st FOCS 1980, pp. 96???107 (1980);","DOI":"10.1109\/SFCS.1980.37"},{"key":"#cr-split#-12_CR36.2","doi-asserted-by":"crossref","unstructured":"Also in: J. Computer and System Sci. 25, 239???266 (1982)","DOI":"10.1016\/0022-0000(82)90006-X"},{"key":"#cr-split#-12_CR37.1","unstructured":"Jouannaud, J.-P., Kounalis, E.: Automatic Proofs by Induction in Equational Theories Without Constructors. In: 1st IEEE symposium on Logi. In: Computer Sci., pp. 358???366. IEEE Press, Los Alamitos, (1986);"},{"key":"#cr-split#-12_CR37.2","unstructured":"Also in: Information and Computation 82, 1???33 (1989)"},{"key":"12_CR38","first-page":"367","volume-title":"1st IEEE symposium on Logic In Computer Sci.","author":"D. Kapur","year":"1986","unstructured":"Kapur, D., Musser, D.R.: Inductive Reasoning with Incomplete Specifications. In: 1st IEEE symposium on Logic In Computer Sci., pp. 367\u2013377. IEEE Press, Los Alamitos (1986)"},{"key":"12_CR39","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0004-3702(87)90017-8","volume":"31","author":"D. Kapur","year":"1987","unstructured":"Kapur, D., Musser, D.R.: Proof by Consistency. Artificial Intelligence\u00a031, 125\u2013157 (1987)","journal-title":"Artificial Intelligence"},{"key":"12_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"559","DOI":"10.1007\/3-540-51081-8_138","volume-title":"Rewriting Techniques and Applications","author":"D. Kapur","year":"1989","unstructured":"Kapur, D., Zhang, H.: An Overview of Rewrite Rule Laboratory (Rrl). In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol.\u00a0355, pp. 559\u2013563. Springer, Heidelberg (1989)"},{"key":"12_CR41","volume-title":"Computer-Aided Reasoning: An Approach","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer, Dordrecht (2000)"},{"key":"12_CR42","first-page":"240","volume-title":"8 th AAAI 1990","author":"E. Kounalis","year":"1990","unstructured":"Kounalis, E., Rusinowitch, M.: Mechanizing Inductive Reasoning. In: 8 th AAAI 1990, pp. 240\u2013245. MIT Press, Cambridge (1990)"},{"key":"12_CR43","first-page":"95","volume-title":"Lectures on Modern Mathematics","author":"G. Kreisel","year":"1965","unstructured":"Kreisel, G.: Mathematical Logic. In: Saaty, T.L. (ed.) Lectures on Modern Mathematics, vol.\u00a0III, pp. 95\u2013195. John Wiley & Sons, New York (1965)"},{"key":"#cr-split#-12_CR44.1","unstructured":"K??chlin, W.: Inductive Completion by Ground Proof Transformation. Colloquium on Resolution of Equations in Algebraic Structures, CREAS (1987);"},{"key":"#cr-split#-12_CR44.2","unstructured":"Also In: [1], Vol. 2, pp. 211???244"},{"key":"12_CR45","unstructured":"K\u00fchler, U.: A Tactic-Based Inductive Theorem Prover for Data Types with Partial Operations. Ph.D. thesis, Infix, Sankt Augustin (2000)"},{"key":"#cr-split#-12_CR46.1","unstructured":"K??hler, U., Wirth, C.-P.: Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving. SEKI Report SR???96???11, Univ. Kaiserslautern (1996);"},{"key":"#cr-split#-12_CR46.2","unstructured":"Short version In: Comon, H. (ed.): RTA 1997. LNCS, vol.??1232, pp. 38???52. Springer, Heidelberg (1997), http:\/\/ags.uni-sb.de\/~cp\/p\/rta97\/welcome.html (August 05, 2001)"},{"key":"12_CR47","unstructured":"Lankford, D.S.: Some Remarks on Inductionless Induction. Memo MTP- 11, Math. Dept., Louisiana Tech. Univ., Ruston (1980)"},{"key":"12_CR48","unstructured":"Lankford, D.S.: A Simple Explanation of Inductionless Induction. Memo MTP-14, Math. Dept., Louisiana Tech. Univ., Ruston (1981)"},{"key":"12_CR49","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF00245018","volume":"5","author":"V.A. Lifschitz","year":"1989","unstructured":"Lifschitz, V.A.: What Is the Inverse Method? J. Automated Reasoning\u00a05, 1\u201323 (1989)","journal-title":"J. Automated Reasoning"},{"key":"12_CR50","doi-asserted-by":"publisher","first-page":"454","DOI":"10.1109\/TSE.1985.232484","volume":"11","author":"D.B. MacQueen","year":"1985","unstructured":"MacQueen, D.B., Sannella, D.T.: Completeness of Proof Systems for Equational Specifications. IEEE Transactions on Software Engineering\u00a011, 454\u2013461 (1985)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"12_CR51","first-page":"154","volume-title":"7 th POPL 1980","author":"D.R. Musser","year":"1980","unstructured":"Musser, D.R.: On Proving Inductive Properties of Abstract Data Types. In: 7 th POPL 1980, pp. 154\u2013162. ACM Press, New York (1980)"},{"key":"12_CR52","first-page":"226","volume":"53","author":"C.F. Nourani","year":"1994","unstructured":"Nourani, C.F.: Types, Induction, and Incompleteness. Bull. EATCS\u00a053, 226\u2013247 (1994)","journal-title":"Bull. EATCS"},{"key":"12_CR53","unstructured":"Padawitz, P.: Horn Logic and Rewriting for Functional and Logic Program Design. MIP\u20139002, Univ. Passau (1990)"},{"key":"12_CR54","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1006\/jsco.1996.0003","volume":"21","author":"P. Padawitz","year":"1996","unstructured":"Padawitz, P.: Inductive Theorem Proving for Design Specifications. J. Symbolic Computation\u00a021, 41\u201399 (1996)","journal-title":"J. Symbolic Computation"},{"key":"12_CR55","unstructured":"Padawitz, P.: Expander. A System for Testing and Verifying Functional Logic Programs (1998), http:\/\/LS5.cs.uni-dortmund.de\/~peter\/ExpaTex.ps.gz (September 14, 1999)"},{"key":"12_CR56","series-title":"LNAI","first-page":"340","volume-title":"Automated Deduction - CADE-11","author":"M. Protzen","year":"1992","unstructured":"Protzen, M.: Disproving Conjectures. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol.\u00a0607, pp. 340\u2013354. Springer, Heidelberg (1992)"},{"key":"12_CR57","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1007\/3-540-58156-1_4","volume-title":"Automated Deduction - CADE-12","author":"M. Protzen","year":"1994","unstructured":"Protzen, M.: Lazy Generation of Induction Hypotheses. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol.\u00a0814, pp. 42\u201356. Springer, Heidelberg (1994); Long version In: [58]"},{"key":"12_CR58","doi-asserted-by":"crossref","unstructured":"Protzen, M.: Lazy Generation of Induction Hypotheses and Patching Faulty Conjectures. Ph.D. thesis, Infix, Sankt Augustin (1995)","DOI":"10.1007\/3-540-61511-3_70"},{"key":"12_CR59","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/3-540-52885-7_86","volume-title":"10th International Conference on Automated Deduction","author":"U.S. Reddy","year":"1990","unstructured":"Reddy, U.S.: Term Rewriting Induction. In: Stickel, M.E. (ed.) CADE 1990. LNCS (LNAI), vol.\u00a0449, pp. 162\u2013177. Springer, Heidelberg (1990)"},{"volume-title":"Handbook of Automated Reasoning","year":"2001","key":"12_CR60","unstructured":"Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning. Elsevier, Amsterdam (2001)"},{"key":"12_CR61","unstructured":"Sprenger, C.: \u00dcber die Beweissteuerung des induktiven Theorembeweisers QuodLibet mit Taktiken. Master\u2019s thesis, FB Informatik, Univ. Kaiserslautern (1996)"},{"key":"12_CR62","unstructured":"Steel, G.: Inductionless Induction (aka Implicit Induction or Proof by Consistency): A Literature Survey (1999), http:\/\/www.dai.ed.ac.uk\/homes\/grahams\/papers\/lit-survey.ps.gz (April 28, 2002)"},{"key":"12_CR63","unstructured":"Steel, G., Bundy, A., Denney, E.: Using Implicit Induction to Guide a Parallel Search for Inconsistency (2002), http:\/\/www.dai.ed.ac.uk\/homes\/grahams\/papers\/abstract.pdf (April 28, 2002)"},{"key":"12_CR64","doi-asserted-by":"crossref","first-page":"47","DOI":"10.3233\/FI-1995-24123","volume":"24","author":"J. Steinbach","year":"1995","unstructured":"Steinbach, J.: Simplification Orderings \u2013 History of Results. Fundamenta Informaticae\u00a024, 47\u201387 (1995)","journal-title":"Fundamenta Informaticae"},{"key":"12_CR65","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1006\/jsco.2000.0469","volume":"32","author":"S. Stratulat","year":"2001","unstructured":"Stratulat, S.: A General Framework to Build Contextual Cover Set Induction Provers. J. Symbolic Computation\u00a032, 403\u2013445 (2001)","journal-title":"J. Symbolic Computation"},{"key":"12_CR66","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/BFb0013076","volume-title":"Logic Programming and Automated Reasoning","author":"C. Walther","year":"1992","unstructured":"Walther, C.: Computing Induction Axioms. In: Voronkov, A. (ed.) LPAR 1992. LNCS (LNAI), vol.\u00a0624, pp. 381\u2013392. Springer, Heidelberg (1992)"},{"key":"12_CR67","doi-asserted-by":"crossref","unstructured":"Walther, C.: Mathematical Induction. In: [24], vol.\u00a02, pp. 127\u2013228 (1994)","DOI":"10.1093\/oso\/9780198537465.003.0003"},{"key":"#cr-split#-12_CR68.1","unstructured":"Wirth, C.-P.: Inductive Theorem Proving in Theories Specified by Positive\/Negative-Conditional Equations. Master???s thesis, FB Informatik, Univ. Kaiserslautern (1991);"},{"key":"#cr-split#-12_CR68.2","unstructured":"Abstract In: 1st Workshop on Construction of Computational Logics, Val d???Ajol (France), 1992, Rapport Interne CRIN 93???R???023, p. 38, Villersles- Nancy (1993)"},{"key":"12_CR69","unstructured":"Wirth, C.-P.: Positive\/Negative-Conditional Equations: A Constructor- Based Framework for Specification and Inductive Theorem Proving. Ph.D. thesis, Verlag Dr. Kova\u010d, Hamburg (1997)"},{"key":"12_CR70","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/3-540-48754-9_25","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"C.-P. Wirth","year":"1999","unstructured":"Wirth, C.-P.: Full First-Order Free Variable Sequents and Tableaus in Implicit Induction. In: Murray, N.V. (ed.) TABLEAUX 1999. LNCS (LNAI), vol.\u00a01617, pp. 293\u2013307. Springer, Heidelberg (1999), http:\/\/ags.uni-sb.de\/~cp\/p\/tab99\/welcome.html (August 05, 2001)"},{"key":"12_CR71","unstructured":"Wirth, C.-P.: Descente Infinie + Deduction. Report 737\/2000, FB Informatik, Univ. Dortmund. Extd. version (2000), http:\/\/ags.uni-sb.de\/~cp\/p\/tab99\/new.html (February 1, 2003)"},{"key":"12_CR72","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/3-540-60381-6_21","volume-title":"Conditional and Typed Rewriting Systems","author":"C.-P. Wirth","year":"1995","unstructured":"Wirth, C.-P., Becker, K.: Abstract Notions and Inference Systems for Proofs by Mathematical Induction. In: Lindenstrauss, N., Dershowitz, N. (eds.) CTRS 1994. LNCS, vol.\u00a0968, pp. 353\u2013373. Springer, Heidelberg (1995), http:\/\/ags.uni-sb.de\/~cp\/p\/ctrs94\/welcome.html"},{"key":"12_CR73","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1006\/jsco.1994.1004","volume":"17","author":"C.-P. Wirth","year":"1994","unstructured":"Wirth, C.-P., Gramlich, B.: A Constructor-Based Approach for Positive\/Negative-Conditional Equational Specifications. J. Symbolic Computation\u00a017, 51\u201390 (1994), http:\/\/ags.uni-sb.de\/~cp\/p\/jsc94\/welcome.html (August 05, 2001)","journal-title":"J. Symbolic Computation"},{"key":"12_CR74","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/3-540-58156-1_12","volume-title":"Automated Deduction - CADE-12","author":"C.-P. Wirth","year":"1994","unstructured":"Wirth, C.-P., Gramlich, B.: On Notions of Inductive Validity for First-Order Equational Clauses. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol.\u00a0814, pp. 162\u2013176. Springer, Heidelberg (1994), http:\/\/ags.uni-sb.de\/~cp\/p\/cade94\/welcome.html"},{"key":"12_CR75","unstructured":"Wirth, C.-P., K\u00fchler, U.: Inductive Theorem Proving in Theories Specified by Positive\/Negative-Conditional Equations. SEKI-Report SR\u201395\u2013 15 (SFB), Univ. Kaiserslautern (1995), http:\/\/ags.uni-sb.de\/~cp\/p\/sr9515\/welcome.html (August 05, 2001)"},{"key":"12_CR76","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/BFb0012831","volume-title":"9th International Conference on Automated Deduction","author":"H. Zhang","year":"1988","unstructured":"Zhang, H., Kapur, D., Krishnamoorthy, M.S.: A Mechanizable Induction Principle for Equational Specifications. In: Lusk, E.\u2018., Overbeek, R. (eds.) CADE 1988. LNCS (LNAI), vol.\u00a0310, pp. 162\u2013181. Springer, Heidelberg (1988)"}],"container-title":["Lecture Notes in Computer Science","Mechanizing Mathematical Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-32254-2_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T04:49:25Z","timestamp":1740199765000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32254-2_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540250517","9783540322542"],"references-count":84,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32254-2_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}