Sufficient-completeness, ground-reducibility and their complexity

1. Book, R.: Confluent and other types of Thue systems. J. Assoc. Comput. Mach.29, 171–182 (1982)

   Google Scholar 

2. Boyer, R.S., Moore, J.S.: A computational logic. New York: Academic Press 1979

   Google Scholar 

3. Comon, H.: Sufficient-completeness, term rewriting systems, and “anti-unification”. Proc. of 8th Intl. Conf. on Automated Deduction (Lect. Notes Comput. Sci., Vol. 230, pp. 128–140). Berlin Heidelberg New York: Springer 1986

   Google Scholar 

4. Cook, S.A.: Characterizations of pushdown machines in terms of time-bounded computers. J. Assoc. Comput. Mach.18, 4–18 (1971)

   Google Scholar 

5. Dershowitz, N.: Computing with rewrite systems. Inf. Control65, 122–157 (1985)

   Google Scholar 

6. Garey, M.R., Johnson, D.S.: Computers and intractability. W.H. Freeman 1979

7. Goguen, J.: How to prove algebraic inductive hypotheses without induction. Proc. of the 5th Conference on Automated Deduction, Les Arcs, France. (Lect. Notes Comput. Sci., Vol. 87, pp. 356–373) Berlin Heidelberg New York: Springer 1980

   Google Scholar 

8. Guttag, J.: The specification and application to programming of abstract data types. Department of Computer Science, Univ. of Toronto, Ph.D. Thesis, CSRG-59 (1975)

9. Guttag, J., Horning, J.J.: The algebraic specification of abstract data types. Acta Inf.10, 27–52 (1978)

   Google Scholar 

10. Huet, G., Hullot, J.M.: Proofs by induction in equational theories with constructors. J. Comput. Syst. Sci.25, 239–266 (1982)

    Google Scholar 

11. Huet, G., Oppen, D.C.: Equations and rewrite rules: A survey. In: R. Book (ed.) Formal language theory: Perspectives and open problems, pp. 349–405. New York: Academic Press 1980

    Google Scholar 

12. Hunt, H.B., Rosenkrantz, D.J.: The complexity of monadic recursion schemes: Exponential time bounds. J. Comput. Syst. Sci.28, 395–419 (1984)

    Google Scholar 

13. Jouannaud, J.-P., Kounalis, E.: Automatic proofs by induction in equational theories without constructors. Proc. of the IEEE Symposium on Logic in Computer Science, Cambridge, Mass, pp. 358–386, 1986

14. Kapur, D., Musser, D.R.: Proof by consistency. Artif. Intell. J.31, 125–157 (1987)

    Google Scholar 

15. Kapur, D., Narendran, P., Zhang, H.: Proof by induction using test sets. Proc. of 8th Intl. Conf. on Automated Deduction, Oxford England (Lect. Notes Comput. Sci., Vol. 230, pp. 99–117) Berlin Heidelberg New York: Springer 1986a

    Google Scholar 

16. Kapur, D., Narendran, P., Zhang, H.: On sufficient-completeness and related properties of term rewriting systems. Acta Inf.24, 395–416 (1987)

    Google Scholar 

17. Kapur, D., Narendran, P., Zhang, H.: Complexity of sufficient-completeness. Proc. of 6th Conf. on Foundations of Software Technology and Theoretical Computer Science, New Delhi, India (Lect. Notes Comput. Sci., Vol. 241, pp. 426–442) Berlin Heidelberg New York: Springer 1986b

    Google Scholar 

18. Knuth, D., Bendix, P.: Simple word problems in universal algebras. In: J. Leech (ed.). Computational problems in abstract algebra, pp. 263–297. Oxford: Pergamon Press (1970)

    Google Scholar 

19. Kounalis, E.: Completeness in data type specifications. Proc. EUROCAL'85, LNCS 204 (Bob F. Caviness, ed.), pp. 348–362. Berlin Heidelberg New York: Springer 1985

    Google Scholar 

20. Lankford, D.S., Ballantyne, A.M.: Decision procedures for simple equational theories with commutative-associative axioms: Complete sets of commutative-associative reductions. Technical Report ATP-39, Dept. of Math. and Computer Science, Univ. of Texas at Austin, Texas, 1977

    Google Scholar 

21. Lankford, D.S.: A simple explanation of inductionless induction. Memo MTP-14, Dept. of Mathematics, Louisiana Tech. University, Ruston, Louisiana, 1981

    Google Scholar 

22. Lassez, J.-L., Marriott, K.: Explicit representation of terms defined by counter-examples. J Automat. Reasoning3, 301–318 (1987)

    Google Scholar 

23. Lewis, H.: Complexity results for classes of quantificational formulas. J. Comput. System Sci.21, 317–353 (1980)

    Google Scholar 

24. Marriott, K.: A note on the complexity of determining the reasonability and the existence of an explicit representation for an implicit generalization. Draft manuscript. Computer Science Dept. University of Melbourne, Australia, 1988

    Google Scholar 

25. Minsky, M.L.: Recursive unsolvability of Post's problem of “Tag” and other topics in theory of Turing machines. Ann. Math.74, 437–455 (1961)

    Google Scholar 

26. Musser, D.R.: On proving inductive properties of abstract data types. Proc. 7th Principles of Programming Languages, Las Vegas, Nevada 1980

27. Nipkow, T., Weikum, G.: A decidability result about sufficient-completeness of axiomatically specified abstract data types. Proc. of the 6th GI Conf. on Theoretical Computer Science, (Lect. Notes Comput. Sci., Vol. 145, pp. 257–268) Berlin Heidelberg New York: Springer 1982

    Google Scholar 

28. Peterson, G.L., Stickel, M.E.: Complete set of reductions for some equational theoris. J. Assoc. Comput. Mach.28, 233–264 (1981)

    Google Scholar 

29. Plaisted, D.: Complete problems in the first-order predicate calculalus. J. Comput. System Sci.29, 8–35 (1984)

    Google Scholar 

30. Plaisted, D.: Semantic confluence tests and completion methods. Inf. Control65, 182–215 (1985)

    Google Scholar 

31. Thiel, J.J.: Stop loosing sleep over incomplete data type specifications. Proc. of Eleventh Annual ACM Symposium on Principles of Programming Languages, Salt Lake City, Utah 1984

Download references