Skip to main content
SpringerLink
Log in

History and Future of Implicit and Inductionless Induction: Beware the Old Jade and the Zombie!

  • Chapter
Mechanizing Mathematical Reasoning

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 2605))

Abstract

In this survey on implicit induction I recollect some memories on the history of implicit induction as it is relevant for future research on computer-assisted theorem proving, esp. memories that significantly differ from the presentation in a recent handbook article on “inductionless induction”. Moreover, the important references excluded there are provided here. In order to clear the fog a little, there is a short introduction to inductive theorem proving and a discussion of connotations of implicit induction like “descente infinie”, “inductionless induction”, “proof by consistency”, implicit induction orderings (term orderings), and refutational completeness.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Ait-Kaci, H., Nivat, M. (eds.): Resolution of Equations in Algebraic Structures. Academic Press, London (1989)

    Google Scholar 

  2. Armando, A., Rusinowitch, M., Stratulat, S.: Incorporating Decision Procedures in Implicit Induction. J. Symbolic Computation 34, 241–258 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  3. Autexier, S., Hutter, D., Mantel, H., Schairer, A.: Inka 5.0 – A Logical Voyager. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 207–211. Springer, Heidelberg (1999)

    Google Scholar 

  4. Avenhaus, J., Madlener, K.: Theorem Proving in Hierarchical Clausal Specifications. SEKI-Report SR–95–14 (SFB), Univ. Kaiserslautern (1995), http://www-madlener.informatik.uni-kl.de/seki/1995/Avenhaus.SR-95-14.ps.gz (March 07, 2002)

  5. Baaz, M., Egly, U., Fermüller, C.G.: Lean Induction Principles for Tableaus. In: Galmiche, D. (ed.) TABLEAUX 1997. LNCS (LNAI), vol. 1227, pp. 62–75. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  6. Bachmair, L.: Proof By Consistency in Equational Theories. In: 3rd IEEE symposium on Logic In Computer Sci., pp. 228–233. IEEE Press, Los Alamitos (1988)

    Google Scholar 

  7. Bachmair, L.: Proof By Consistency. Birkhauser, Boston (1991)

    Google Scholar 

  8. 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. 668, pp. 46–60. Springer, Heidelberg (1993)

    Google Scholar 

  9. Becker, K.: Rewrite Operationalization of Clausal Specifications with Predefined Structures. Ph.D. thesis, FB Informatik, Univ. Kaiserslautern (1994)

    Google Scholar 

  10. Becker, K.: How to Prove Ground Confluence. SEKI-Report SR–96–02, Univ. Kaiserslautern (1996)

    Google Scholar 

  11. Berghammer, R.: On the Characterization of the Integers: The Hidden Function Problem Revisited. Acta Cybernetica 11, 85–96 (1993) (szeged)

    MATH  MathSciNet  Google Scholar 

  12. Bevers, E., Lewi, J.: Proof by Consistency in Conditional Equational Theories. Report CW 102, rev., Dept. Comp. Sci., K. U. Leuven (July 1990); Short version In: Okada, M., Kaplan, S. (eds.): CTRS 1990. LNCS, vol. 516, pp.194-205. Springer, Heidelberg (1991)

    Google Scholar 

  13. Bouhoula, A., Rusinowitch, M.: Implicit Induction in Conditional Theories. J. Automated Reasoning 14, 189–235 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  14. Bouhoula, A., Kounalis, E., Rusinowitch, M.: Automated Mathematical Induction. Technical Report 1636, INRIA (1992)

    Google Scholar 

  15. Boyer, R.S., Moore, J.S.: A Computational Logic. Academic Press, London (1979)

    MATH  Google Scholar 

  16. Boyer, R.S., Moore, J.S.: A Computational Logic Handbook. Academic Press, London (1988)

    MATH  Google Scholar 

  17. 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. F 55, pp. 95–145. Springer, Heidelberg (1989)

    Google Scholar 

  18. Bundy, A.: The Use of Explicit Proof Plans to Guide Inductive Proofs. In: Lusk, E.‘., Overbeek, R. (eds.) CADE 1988. LNCS (LNAI), vol. 310, pp. 111–120. Springer, Heidelberg (1988)

    Chapter  Google Scholar 

  19. Comon, H.: Inductionless induction. In: [60], vol. I, pp. 913–970 (2001)

    Google Scholar 

  20. Comon, H., Nieuwenhuis, R.: Induction = I-Axiomatization + First-order Consistency. Technical Report, ENS Cachan (1998)

    Google Scholar 

  21. Fraus, U.: A Calculus for Conditional Inductive Theorem Proving. In: Rusinowitch, M., Remy, J.-L. (eds.) CTRS 1992. LNCS, vol. 656, pp. 357–362. Springer, Heidelberg (1993)

    Google Scholar 

  22. Fraus, U.: Mechanizing Inductive Theorem Proving in Conditional Theories. Ph.D. thesis, Univ. Passau (1994)

    Google Scholar 

  23. Fribourg, L.: A Strong Restriction of the Inductive Completion Procedure. In: Kott, L. (ed.) ICALP 1986. LNCS, vol. 226, pp. 105–116. Springer, Heidelberg (1986); Also in: J. Symbolic Computation 8, 253–276 (1989)

    Google Scholar 

  24. Gabbay, D.M., Hogger, C.J., Robinson, J.A. (eds.): Handbook of Logic in Artificial Intelligence and Logic Programming. Clarendon Press, Oxford (1993ff.)

    MATH  Google Scholar 

  25. 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); Also In: Rusinowitch, M., Remy, J.-L. (eds.): CTRS 1992. LNCS, vol. 656. Springer, Heidelberg (1993)

    Google Scholar 

  26. Gentzen, G.: Die gegenwärtige Lage in der mathematischen Grundlagenforschung – Neue Fassung des Widerspruchsfreiheitsbeweises für die reine Zahlentheorie. Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften, Folge 4, Leipzig (1938)

    Google Scholar 

  27. Gentzen, G.: Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der transfiniten Induktion in der reinen Zahlentheorie. Mathematische Annalen 119, 140–161 (1943)

    Article  MATH  MathSciNet  Google Scholar 

  28. Geser, A.: A Principle of Non-Wellfounded Induction. In: Margaria, T. (ed.) Kolloquium Programmiersprachen und Grundlagen der Programmierung, MIP–9519, pp. 117–124. Univ. Passau. (1995)

    Google Scholar 

  29. Giese, M.: Integriertes automatisches und interaktives Beweisen: die Kalkülebene. Master’s thesis, Univ. Karlsruhe (1998), http://i11www.ira.uka.de/~giese/da.ps.gz (May 09, 2000)

  30. Göbel, R.: Completion of Globally Finite Term Rewriting Systems for Inductive Proofs. In: 9th German Workshop on AI, IFB 118. Springer, Heidelberg (1985)

    Google Scholar 

  31. Gödel, K.: Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik 38, 173–198 (1931)

    Article  Google Scholar 

  32. Goguen, J.: How to Prove Algebraic Inductive Hypotheses Without Induction. In: Bibel, W. (ed.) CADE 1980. LNCS, vol. 87, pp. 356–373. Springer, Heidelberg (1980)

    Google Scholar 

  33. Gramlich, B.: Inductive Theorem Proving Using Refined Unfailing Completion Techniques. SEKI-Report SR–89–14 (SFB), Univ. Kaiserslautern (1989); Short version In: 9th ECAI 1990, pp. 314–319. Pitman Publ. (1990)

    Google Scholar 

  34. Gramlich, B.: Completion Based Inductive Theorem Proving: A Case Study in Verifying Sorting Algorithms. SEKI-Report SR–90–04, Univ. Kaiserslautern (1990)

    Google Scholar 

  35. Gramlich, B., Lindner, W.: A Guide to Unicom, an Inductive Theorem Prover Based on Rewriting and Completion Techniques. SEKI-Report SR-91–17 (SFB) Univ. Kaiserslautern (1991), http://agent.informatik.uni-kl.de/seki/1991/Lindner.SR-91-17.ps.gz (May 09, 2000)

  36. Huet, G., Hullot, J.-M.: Proofs by Induction in Equational Theories with Constructors. In: 21st FOCS 1980, pp. 96–107 (1980); Also in: J. Computer and System Sci. 25, 239–266 (1982)

    Google Scholar 

  37. 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); Also in: Information and Computation 82, 1–33 (1989)

    Google Scholar 

  38. Kapur, D., Musser, D.R.: Inductive Reasoning with Incomplete Specifications. In: 1st IEEE symposium on Logic In Computer Sci., pp. 367–377. IEEE Press, Los Alamitos (1986)

    Google Scholar 

  39. Kapur, D., Musser, D.R.: Proof by Consistency. Artificial Intelligence 31, 125–157 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  40. Kapur, D., Zhang, H.: An Overview of Rewrite Rule Laboratory (Rrl). In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol. 355, pp. 559–563. Springer, Heidelberg (1989)

    Google Scholar 

  41. Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer, Dordrecht (2000)

    Google Scholar 

  42. Kounalis, E., Rusinowitch, M.: Mechanizing Inductive Reasoning. In: 8th AAAI 1990, pp. 240–245. MIT Press, Cambridge (1990)

    Google Scholar 

  43. Kreisel, G.: Mathematical Logic. In: Saaty, T.L. (ed.) Lectures on Modern Mathematics, vol. III, pp. 95–195. John Wiley & Sons, New York (1965)

    Google Scholar 

  44. Küchlin, W.: Inductive Completion by Ground Proof Transformation. Colloquium on Resolution of Equations in Algebraic Structures, CREAS (1987); Also In: [1], Vol. 2, pp. 211–244

    Google Scholar 

  45. Kühler, U.: A Tactic-Based Inductive Theorem Prover for Data Types with Partial Operations. Ph.D. thesis, Infix, Sankt Augustin (2000)

    Google Scholar 

  46. 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); 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)

  47. Lankford, D.S.: Some Remarks on Inductionless Induction. Memo MTP- 11, Math. Dept., Louisiana Tech. Univ., Ruston (1980)

    Google Scholar 

  48. Lankford, D.S.: A Simple Explanation of Inductionless Induction. Memo MTP-14, Math. Dept., Louisiana Tech. Univ., Ruston (1981)

    Google Scholar 

  49. Lifschitz, V.A.: What Is the Inverse Method? J. Automated Reasoning 5, 1–23 (1989)

    Article  MATH  MathSciNet  Google Scholar 

  50. MacQueen, D.B., Sannella, D.T.: Completeness of Proof Systems for Equational Specifications. IEEE Transactions on Software Engineering 11, 454–461 (1985)

    Article  MathSciNet  Google Scholar 

  51. Musser, D.R.: On Proving Inductive Properties of Abstract Data Types. In: 7th POPL 1980, pp. 154–162. ACM Press, New York (1980)

    Google Scholar 

  52. Nourani, C.F.: Types, Induction, and Incompleteness. Bull. EATCS 53, 226–247 (1994)

    MATH  Google Scholar 

  53. Padawitz, P.: Horn Logic and Rewriting for Functional and Logic Program Design. MIP–9002, Univ. Passau (1990)

    Google Scholar 

  54. Padawitz, P.: Inductive Theorem Proving for Design Specifications. J. Symbolic Computation 21, 41–99 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  55. 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)

  56. Protzen, M.: Disproving Conjectures. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol. 607, pp. 340–354. Springer, Heidelberg (1992)

    Google Scholar 

  57. Protzen, M.: Lazy Generation of Induction Hypotheses. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol. 814, pp. 42–56. Springer, Heidelberg (1994); Long version In: [58]

    Google Scholar 

  58. Protzen, M.: Lazy Generation of Induction Hypotheses and Patching Faulty Conjectures. Ph.D. thesis, Infix, Sankt Augustin (1995)

    Google Scholar 

  59. Reddy, U.S.: Term Rewriting Induction. In: Stickel, M.E. (ed.) CADE 1990. LNCS (LNAI), vol. 449, pp. 162–177. Springer, Heidelberg (1990)

    Google Scholar 

  60. Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning. Elsevier, Amsterdam (2001)

    MATH  Google Scholar 

  61. Sprenger, C.: Über die Beweissteuerung des induktiven Theorembeweisers QuodLibet mit Taktiken. Master’s thesis, FB Informatik, Univ. Kaiserslautern (1996)

    Google Scholar 

  62. 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)

  63. 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)

  64. Steinbach, J.: Simplification Orderings – History of Results. Fundamenta Informaticae 24, 47–87 (1995)

    MATH  MathSciNet  Google Scholar 

  65. Stratulat, S.: A General Framework to Build Contextual Cover Set Induction Provers. J. Symbolic Computation 32, 403–445 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  66. Walther, C.: Computing Induction Axioms. In: Voronkov, A. (ed.) LPAR 1992. LNCS (LNAI), vol. 624, pp. 381–392. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  67. Walther, C.: Mathematical Induction. In: [24], vol. 2, pp. 127–228 (1994)

    Google Scholar 

  68. Wirth, C.-P.: Inductive Theorem Proving in Theories Specified by Positive/Negative-Conditional Equations. Master’s thesis, FB Informatik, Univ. Kaiserslautern (1991); 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)

    Google Scholar 

  69. Wirth, C.-P.: Positive/Negative-Conditional Equations: A Constructor- Based Framework for Specification and Inductive Theorem Proving. Ph.D. thesis, Verlag Dr. Kovač, Hamburg (1997)

    Google Scholar 

  70. Wirth, C.-P.: Full First-Order Free Variable Sequents and Tableaus in Implicit Induction. In: Murray, N.V. (ed.) TABLEAUX 1999. LNCS (LNAI), vol. 1617, pp. 293–307. Springer, Heidelberg (1999), http://ags.uni-sb.de/~cp/p/tab99/welcome.html (August 05, 2001)

    Chapter  Google Scholar 

  71. 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)

  72. 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. 968, pp. 353–373. Springer, Heidelberg (1995), http://ags.uni-sb.de/~cp/p/ctrs94/welcome.html

    Google Scholar 

  73. Wirth, C.-P., Gramlich, B.: A Constructor-Based Approach for Positive/Negative-Conditional Equational Specifications. J. Symbolic Computation 17, 51–90 (1994), http://ags.uni-sb.de/~cp/p/jsc94/welcome.html (August 05, 2001)

    Article  MATH  MathSciNet  Google Scholar 

  74. Wirth, C.-P., Gramlich, B.: On Notions of Inductive Validity for First-Order Equational Clauses. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol. 814, pp. 162–176. Springer, Heidelberg (1994), http://ags.uni-sb.de/~cp/p/cade94/welcome.html

    Google Scholar 

  75. Wirth, C.-P., Kühler, U.: Inductive Theorem Proving in Theories Specified by Positive/Negative-Conditional Equations. SEKI-Report SR–95– 15 (SFB), Univ. Kaiserslautern (1995), http://ags.uni-sb.de/~cp/p/sr9515/welcome.html (August 05, 2001)

  76. Zhang, H., Kapur, D., Krishnamoorthy, M.S.: A Mechanizable Induction Principle for Equational Specifications. In: Lusk, E.‘., Overbeek, R. (eds.) CADE 1988. LNCS (LNAI), vol. 310, pp. 162–181. Springer, Heidelberg (1988)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Computer Science, Universität des Saarlandes, D–66123, Saarbrücken, Germany

    Claus-Peter Wirth

Authors
  1. Claus-Peter Wirth
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. DFKI, Stuhlsatzenhausweg 3, D-66123, Saarbrücken, Germany

    Dieter Hutter

  2. German Research Center for Artificial Intelligence, DFKI GmbH,  

    Werner Stephan

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Wirth, CP. (2005). History and Future of Implicit and Inductionless Induction: Beware the Old Jade and the Zombie!. In: Hutter, D., Stephan, W. (eds) Mechanizing Mathematical Reasoning. Lecture Notes in Computer Science(), vol 2605. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-32254-2_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-32254-2_12

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-25051-7

  • Online ISBN: 978-3-540-32254-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation