Proof normalization for resolution and paramodulation

1. Bachmair, L. 1987. Proof methods for equational theories. Ph.D. diss., University of Illinois, Urbana-Champaign.

   Google Scholar 

2. Bachmair, L., Dershowitz, N., and Hsiang, J. 1986. Orderings for equational proofs. In Proc. Symp. Logic in Computer Science, Boston, Massachusetts, 346–357.

   Google Scholar 

3. Brand, D. 1975. Proving theorems with the modification method. SIAM J. Comput.4:412–430.

   Google Scholar 

4. Brown, T. 1975. A structured design-method for specialized proof procedures. Ph.D. diss., California Institute of Technology, Pasadena.

   Google Scholar 

5. Chang, C., and Lee, R. C. 1973. Symbolic logic and mechanical theorem proving. New York, Academic Press.

   Google Scholar 

6. Dershowitz, N. 1982. Orderings for term-rewriting systems. Theor. Comput. Sci.17:279–301.

   Google Scholar 

7. Dershowitz, N. 1987. Termination of rewriting. J. Symbolic Computation3:69–116.

   Google Scholar 

8. Dershowitz, N., and Manna, Z. 1979. Proving termination with multiset orderings. Commun. ACM22:465–476.

   Google Scholar 

9. Ganzinger, H. 1988. A completion procedure for conditional equations. To appear in J. Symbolic Computation.

   Google Scholar 

10. Hsiang, J., and Rusinowitch, M. 1986. A new method for establishing refutational completeness in theorem proving. In Proc. 8th Int. Conf. on Automated Deduction, ed. J. H. Siekmann, Lect. Notes in Comput. Sci., vol. 230, Berlin, Springer-Verlag, 141–152.

    Google Scholar 

11. Hsiang, J., and Rusinowitch, M. 1988. Proving refutational completeness of theorem proving strategies, Part I: The transfinite semantic tree method. Submitted for publication.

    Google Scholar 

12. Joyner, W. 1976. Resolution strategies as decision procedures. J. ACM23:398–417.

    Google Scholar 

13. Knuth, D., and Bendix, P. 1970. simple word problems in universal algebras. In Computational Problems in Abstract Algebra, ed. J. Leech, Oxford, Pergamon Press, 263–297.

    Google Scholar 

14. Lankford, D. 1975. Canonical inference. Tech. Rep. ATP-32, Dept. of Mathematics and Computer Science, University of Texas, Austin.

    Google Scholar 

15. Peterson, G. 1983. A technique for establishing completeness results in theorem proving with equality. SIAM J. Comput.12:82–100.

    Google Scholar 

16. Robinson, G., and Wos, L. T. 1969. Paramodulation and theorem proving in first order theories with equality. In Machine Intelligence 4, ed. B. Meltzer and D. Michie, New York, American Elsevier, 133–150.

    Google Scholar 

17. Robinson, J. A. 1965. A machine-oriented logic based on the resolution principle. J. ACM12:23–41.

    Google Scholar 

18. Rusinowitch, M. 1988. Theorem proving with resolution and superposition: An extension of the Knuth and Bendix procedure as a complete set of inference rules.

    Google Scholar 

19. Slagle, J. R. 1974. Automated theorem proving for theories with simplifiers, commutativity, and associativity. J. ACM21:622–642.

    Google Scholar 

20. Wos, L. T., and Robinson, G. 1973. Maximal models and refutation completeness: Semidecision procedures in automatic theorem proving. In Word Problems, ed. W.W. Boone et al., Amsterdam, North-Holland, 609–639.

    Google Scholar 

21. Wos, L. T., Robinson, G. A., Carson, D. F., and Shalla, L. 1967. The concept of demodulation in theorem proving. J. ACM14:698–709.

    Google Scholar 

22. Zhang, H., and Kapur, D. 1988. First-order theorem proving using conditional rewrite rules. In Proc. 9th Conf. Automated Deduction, Let. Notes in Comput. Sci. Berlin, Springer-Verlag, 1–20.

    Google Scholar 

Download references