Proving Ramsey's theorem by the cover set induction: A case and comparison study

1. D. Basin and M. Kaufmann, The Boyer-Moore prover and Nuprl: an experimental comparison, in:Proc. BRA Logical Frameworks Workshop (1990).

2. J. Bondy and R. Murthy,Graph Theory with Applications (American Elsevier, 1976).

3. R.S. Boyer and J.S. Moore,A Computational Logic (Academic Press, New York, 1979).

   Google Scholar 

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

   Google Scholar 

5. R.S. Boyer and J.S. Moore, Overview of a theorem-prover for a computational logic, in:Proc. 8th Int. Conf. on Automated Deduction (CADE-8), Oxford, UK, (1986) (Springer, LNCS 230).

6. R.L. Constable et al.,Implementing Mathematics with the Nuprl Proof Development System (Prentice-Hall, Englewood Cliffs, NJ, 1986).

   Google Scholar 

7. N. Dershowitz, Termination of rewriting, J. Symbolic Comput. 3(1987)69–116.

   Google Scholar 

8. N. Dershowitz and J.-P. Jouannaud, Rewrite systems, in:Handbook of Theoretical Computer Science B: Formal Methods and Semantics, ed. J. van Leeuwen (North-Holland, Amsterdam, 1990) chap. 6 pp. 243–320.

   Google Scholar 

9. J.A. Goguen, J.W. Thatcher and E.W. Wagner, Initial algebra approach to the specification, correctness, and implementation of abstract data types, in:Data Structuring, Current Trends in Programming Methodology,4, ed. R.T. Yeh (Prentice-Hall, Englewood Cliffs, NJ, 1978).

   Google Scholar 

10. J.V. Guttag and J.J. Horning, The algebraic specification of abstract data types, Acta Informatica 10(1978)27–52.

    Google Scholar 

11. G. Huet and J.M. Hullot, Proofs by induction in equational theories with constructors, in:21st IEEE Symp. on Foundations of Computer Science, Syracuse, NY (1980) pp. 96–107.

12. J.-P. Jouannaud and E. Kounalis, Proofs by induction in equational theories without constructors, in:Proc. of Logic in Computer Science Conf., Cambridge, MA (1986).

13. D. Kapur and D. Musser, Proof by consistency, Artificial Intelligence 31(1987)125–157.

    Google Scholar 

14. D. Kapur, P. Narendran and H. Zhang, On sufficient completeness and related properties of term rewriting systems, Acta Informatica 24(1987)395–415.

    Google Scholar 

15. D. Kapur, P. Narendran and H. Zhang, Proof by induction using test sets,Proc. 8th Int. Conf. on Automated Deduction (CADE-8), Oxford, UK, 1986 (Springer, LNCS 230) pp. 99–117.

16. D. Kapur and H. Zhang, An overview of RRL: Rewrite Rule Laboratory,Proc, 3rd Int. Conf. on Rewriting Techniques and Their Applications (RTA-89), Chapel Hill, NC, 1989 (Springer, LNCS 355) pp. 513–529.

17. M. Kaufmann, An interactive enhancement to the Boyer-Moore theorem prover, in:Proc. 9th Int. Conf. on Automated Deduction (CADE-9), Argonne, IL, 1988 (Springer, LNCS 310) pp. 735–736.

18. E. Kounalis and M. Rusinowitch, Mechanizing inductive reasoning, in:Proc. American Association for Artificial Intelligence Conf., Boston (AAAI Press and MIT Press, 1990) pp. 240–245.

19. D, Musser, On proving inductive properties of abstract data types,Proc. 7th Principles of Programming Languages, Las Vegas (1980).

20. M. O'Donnell,Equational Logic as a Programming Language (MIT Press, Cambridge, 1985).

    Google Scholar 

21. H. Zhang and D. Kapur, First-order logic theorem proving using conditional rewrite rules, in:Proc. 9th Int. Conf. on Automated Deduction (CADE-9), ed. Lusk and Overbeek, Argonne, IL, 1988 (Springer, LNCS 310) pp. 1–20.

22. H. Zhang, D. Kapur and M.S. Krishnamoorthy, A mechanizable induction principle for equational specifications,Proc. 9th Int. Conf. on Automated Deduction (CADE-9), Argonne, IL, 1988 (Springer, LNCS 310) pp. 250–265.

23. H. Zhang, Reduction, superposition and induction: Automated reasoning in an equational logic, Ph.D. Thesis, Rensselear Polytechnic Institute, New York (1988). Accepted for publication in the series ofLecture Notes in Artificial Intelligence (Springer, Berlin).

    Google Scholar 

24. H. Zhang, Implementing contextual rewriting, in:Proc. 3rd Workshop on Conditional Rewriting Systems, ed. M. Rusinowitch and J.L. Remy, 1992 (Springer LNCS 656) pp. 363–377.

25. H. Zhang and X. Hua, Proving the Chinese remainder theorem by the cover set induction, in:Proc. 11th Int. Conf. on Automated Deduction, Saratoga, NY, ed. D. Kapur, 1992 (Springer, LNAI 607) pp. 431–445.

Download references