An overview of LP, the Larch Prover

1. Ben Cherifa, A. and Lescanne, P. “An Actual Implementation of a Procedure that Mechanically Proves Termination of Rewriting Systems Based on Inequalities between Polynomial Interpretations,” Proc. 8th Int. Conf. on Automated Deduction, Oxford, England, LNCS 230, July 1986, 42–51.

   Google Scholar 

2. Boyer, R. S. and Moore, J. S. A Computational Logic, Academic Press, 1979.

   Google Scholar 

3. Dershowitz, N. “Orderings for Term-Rewriting Systems,” Theoretical Computer Science 17:3 (March 1982), 279–301.

   Google Scholar 

4. Detlefs, D. and Forgaard, R. “A Procedure for Automatically Proving the Termination of a Set of Rewrite Rules,” Proc. 1st Int. Conf. on Rewriting Techniques and Applications, Dijon, France, LNCS 202, May 1985, 255–270.

   Google Scholar 

5. Garland, S. J. and Guttag, J. V. “Inductive Methods for Reasoning about Abstract Data Types,” Proc. 15th ACM Conf. on Principles of Programming Languages, San Diego, California, January 1988, 219–228.

   Google Scholar 

6. Garland, S. J., Guttag, J. V. and Staunstrup, J. “Verification of VLSI Circuits Using LP,” Proc. Int. Workshop on Design for Behavioral Verification, July, 1988.

   Google Scholar 

7. Guttag, J.V., Horowitz, E. and Musser, D. R. “Abstract Data Types and Software Validation,” CACM 21:12 (December 1978), 1048–1064.

   Google Scholar 

8. Guttag, J. V. and Horning, J. J. “Report on the Larch Shared Language” and “A Larch Shared Language Handbook,” Sci. Computer Programming 6:2 (March 1986), 103–157.

   Google Scholar 

9. Hsiang, J. and Dershowitz, N. “Rewrite Methods for Clausal and Nonclausal Theorem Proving,” Proc. 10th EATCS Int. Colloquium on Automata, Languages, and Programming, Barcelona, Spain, LNCS 154, July 1983, 331–346.

   Google Scholar 

10. Huet, G. and Hullot, J. M. “Proofs by Induction in Equational Theories with Constructors,” J. Computer and System Sciences 25:2 (October 1982), 239–266.

    Google Scholar 

11. Kapur, D. and Musser, D. R. “Proof by Consistency,” Artificial Intelligence 31 (1987), 125–157.

    Google Scholar 

12. Knuth, D. E. and Bendix, P. B. “Simple Word Problems in Universal Algebras,” in Computational Problems in Abstract Algebra, J. Leech (ed.), Pergamon Press, Oxford, England, 1969, 263–297.

    Google Scholar 

13. Lescanne, P. “Uniform Termination of Term Rewriting Systems: Recursive Decomposition Ordering with Status,” Proc. 6th Colloquium on Trees in Algebra and Programming, Bordeaux, France, Cambridge University Press, March 1984.

    Google Scholar 

14. Lescanne, P. “REVE: A Rewrite Rule Laboratory,” Proc. 8th Int. Conference on Automated Deduction, Oxford, England, LNCS 230, July 1986, 695–696.

    Google Scholar 

15. Musser, D. R. “On Proving Inductive Properties of Abstract Data Types,” Proc. 7th ACM Conference on Principles of Programming Languages, Las Vegas, Nevada, January 1980, 154–162.

    Google Scholar 

16. Paulson, L. C. “The Foundation of a Generic Theorem Prover,” Technical Report No. 130, University of Cambridge Computer Laboratory, March 1988.

    Google Scholar 

17. Peterson, G. L. and Stickel, M. E. “Complete Sets of Reductions for Some Equational Theories,” JACM 28:2 (Apr. 1981), 233–264.

    Google Scholar 

18. Saxe, J. Private communication.

    Google Scholar 

19. Stickel, M. E. “A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering that x ³=x Implies Ring Commutativity,” Proc. 7th Int. Conf. on Automated Deduction, Napa, California, LNCS 170, May 1984, 248–258.

    Google Scholar 

20. Yelick, K. A. “Unification in Combinations of Collapse-Free Regular Theories,” J. Symbolic Computation 3 (1987), 153–181.

    Google Scholar 

21. Zhegalkin, I.I. “On a technique of evaluation of propositions in symbolic logic,” Matematisheskii Sbornik 34:1 (1927), 9–27.

    Google Scholar 

Download references