Skip to main content
SpringerLink
Log in

Mechanizable inductive proofs for a class of ∀ ∃ formulas

  • Conference paper
  • First Online:
Automated Deduction — CADE-12 (CADE 1994)

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

Included in the following conference series:

Abstract

We show how to prove formulas of the form ∀ x∃ yΦ(x, y) in the initial model of an equational variety by using purely algebraic simplifications. This allows to tackle theorems whose proofs requires complicated noetherian induction. We also give a disproof theorem, which is not only useful to prove that a conjecture is false but is also used to shorten the proof search of a theorem. We show applications of the method to fragments of arithmetic.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bachmair, L. Proof by consistency in equational theories, Proc. 3th IEEE Symposium on Logic in Computer Science, Edinburgh.

    Google Scholar 

  2. Bouhala, A. Kounalis, E. and Rusinowitch, M. (1992). Automated Mathematical induction, Research Report of INRIA, Submitted.

    Google Scholar 

  3. Bouhala, A. and Rusinowitch, M. Automatic Case Analysis in Proof by Induction. Int. Joint Conf. on Artificial Intelligence Chambery, 1993.

    Google Scholar 

  4. Boyer, R.S. and Moore, J.S. A Computational Logic, Academic Press, New York.

    Google Scholar 

  5. Bundy, A. and van Harmelen, F. and Smaill A. and Ireland A. Extensions to the rippling-out tactic for guiding inductive proofs. Proc. 10th CADE, LNCS volume 449 (1989).

    Google Scholar 

  6. Burstall, R.M: Proving properties of programs by structural induction. Computer Journal, 12(1), pp. 41–48, 1969.

    Google Scholar 

  7. Dershowitz, N. Termination of rewriting, Journal of Symbolic Computation 3 (1–2).

    Google Scholar 

  8. Dershowitz, N. and Manna, Z. Proving termination with multiset orderings. CACM 22(8), 69–116 (1987).

    Google Scholar 

  9. Dershowitz, N. and Reddy, U. Deductive and Inductive Synthesis of Equational Programs. J. Symbolic Computation (1993) 15, 467–494.

    Google Scholar 

  10. Fribourg, L. A Strong Restriction of the Inductive Completion Procedure, Proc. 13th ICALP, Rennes

    Google Scholar 

  11. Garland, S. J. and Guttag, J.V. Inductive methods for reasoning about abstract data types.” Proc. ACM POPL Conference, (1988)

    Google Scholar 

  12. Huet, G. and Hullot, J.M. (1982). Proofs by induction in equational theories with constructors, Journal of Computer System Sciences 25 (2).

    Google Scholar 

  13. Jouanaud, J.P. and Kounalis, E. (1986 and 1989). Automatic Proofs by induction in equational theories without constructors, Proc. 1st IEEE Symposium on Logic in Computer Science. Full paper in Information and Control 82 (1989).

    Google Scholar 

  14. Kapur, D., Narendran, P. and Zhang, H. Proof by induction with test sets, Proc. 8th CADE, LNCS volume 230 (1986).

    Google Scholar 

  15. Kapur, D.,Krishnamoorthy. and Zhang, H. A mechanizable induction principle for equational specifications”, Proc. 9th CADE, LNCS volume 310 (1988).

    Google Scholar 

  16. Kounalis, E. Pumping lemmas for tree languages generated by rewrite systems, Proc. 15th Conference on Mathematical Foundations of Computer Science (MFCS 90), Banska Bystrica, LNCS 452, Springer-Verlag.

    Google Scholar 

  17. Kounalis, E. Testing for inductive-(co)-reducibility in rewrite systems, Proc. 15th Colloquium on Trees in Algebra and Programming (CAAP 90),LNCS 431, Full paper in Theoretical Computer Science, 1992.

    Google Scholar 

  18. Kounalis, E. and Rusinowitch, M. Mechanizing Inductive Reasoning, Proc. 8th National Conference on Artificial Intelligence (AAAI-90), Boston(USA). Also in the Bulletin of the European Association of Theoretical Computer Science (EATCS), n 41, June 1990.

    Google Scholar 

  19. Musser, D.R. On proving inductive properties of abstract data types, Proc. 7th POPL Conference, Las Vegas (1980).

    Google Scholar 

  20. Padawitz, P., Computing with Horn Clauses, Springer-Verlag 1988.

    Google Scholar 

  21. Reddy, U. Term rewriting induction, Proc. 10th CADE, LNCS volume 449 (1989).

    Google Scholar 

  22. Wainer, S. Computability-Logical and Recursive Complexity. NATO ASI Series. Logic, Algebra and Computation. Edited by F. L. Bauer. Springer Verlag 1991.

    Google Scholar 

  23. Walther, G. Argument-bounded algorithms as bases for automated termination proofs, Proc. 9th CADE, LNCS volume 310 (1988).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratoire d'Informatique I3S, Université de Nice Sophia Antipolis, Bat 4–250 Av. Albert Einstein, 06560, Valbonne, France

    Jacques Chazarain & Emmanuel Kounalis

Authors
  1. Jacques Chazarain
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Emmanuel Kounalis
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Alan Bundy

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Chazarain, J., Kounalis, E. (1994). Mechanizable inductive proofs for a class of ∀ ∃ formulas. In: Bundy, A. (eds) Automated Deduction — CADE-12. CADE 1994. Lecture Notes in Computer Science, vol 814. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58156-1_9

Download citation

  • DOI: https://doi.org/10.1007/3-540-58156-1_9

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-48467-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation