Mechanizable inductive proofs for a class of ∀ ∃ formulas

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