Advertisement

A Narrowing Procedure for Theories with Constructors

  • L. Fribourg
Part of the Lecture Notes in Computer Science book series (LNCS, volume 170)

Abstract

This paper describes methods to prove equational clauses (disjunctions of equations and inequations) in the initial algebra of an equational theory presentation. First we show that the general problem of validity can be converted into the one of satisfiability. Then we present specific procedures based on the narrowing operation, which apply when the theory is defined by a canonical set of rewrite rules. Complete refutation procedures are described and used as invalidity procedures. Finally, a narrowing procedure incorporating structural induction aspects, is proposed and the simplicity of the automated proofs is illustrated through examples.

Keywords

Ground Term Structural Induction Empty Clause Automate Proof Initial Algebra 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [Au]
    Aubin R., “Mechamzing Structural induction”, TCS 9, 1979.Google Scholar
  2. [Bi]
    Bidoit M, “Proofs by induction in “fairly” specified equational theories”, Proc. 6th German Workshop on Artificial Intelligence, Sept. 1982, pp 154–166.Google Scholar
  3. [BM]
    Boyer R., Moore J.S., A computational logic, Academic press, 1979.Google Scholar
  4. [Bu]
    Burstall R.M., “Proving properties of program by structural induction”, Comput. J 12, 1969.Google Scholar
  5. [De1]
    Dershowitz N., “Ordering for term rewriting systems”, TCS 17-3, 1982, pp 279–301.Google Scholar
  6. [De2]
    Dershowitz N., “Computing with Rewrite Systems”, Report No ATR-83 (8478)-1, The Aerospace Corporation, El Segundo, California, 1983.zbMATHGoogle Scholar
  7. [Fa]
    Fages F, “Associative-commutative Unification”, Proc. CADE-7, 1984.Google Scholar
  8. [Fr]
    Fribourg L., “A Superposition Oriented Theorem Prover”, Proc. IJCAI-83, pp923–925.Google Scholar
  9. [Go]
    Goguen J.A., “How to Prove Algebraic Inductive Hypotheses Without Induction, with Applications to the Correctness of Data Type Implementation”, Proc. CADE 5, Los Arcs, July 1980.Google Scholar
  10. [HH]
    Huet G., Hullot J.M., “Proofs by induction in equational theories with constructors”, 21st FOCS, 1980, pp 96–107Google Scholar
  11. [HO]
    Huet G., Oppen D., “Equations and Rewrite Rules: A Survey”, Formal Languages Perspective and Open Problems, Ed. Book R, Academic Press, 1980, pp 349–406Google Scholar
  12. [JLR]
    Jouannaud J.P., Lescanne P., Reinig F., “Recursive Decomposition Ordering”, Formal description of programming concepts 2, Ed. Bjorner, North-Holland, 1982.Google Scholar
  13. [Jo]
    Joyner W.H., “Resolution Strategies as Decision Procedures” J.ACM 23:3, Jul. 1976.Google Scholar
  14. [Ka]
    Kaplan S., “Conditional Rewrite Rule Systems and Termination”, Report L.R.I, Orsay (to appear).Google Scholar
  15. [KB]
    Knuth D., Bendix P., “Simple Word Problems in Universal Algebras”, Computational Problems in Abstract Algebras, Pergamon Press, 1970, pp 263–297.Google Scholar
  16. [KC]
    Kodratoff Y., Castaing J., “Trivializing the proof of trivial theorems”, Proc. IJCAI-83, pp 930–932.Google Scholar
  17. [KK]
    Kowalski R., Kuehner D., “Linear Resolution with Selection Function”, Artif. Intelligence 2, 1971, pp 227–260.MathSciNetCrossRefzbMATHGoogle Scholar
  18. [La]
    Lankford D, “Canonical Inference”, Report ATP-32, U. of Texas, 1975.Google Scholar
  19. [Lo]
    Loveland D., “Automated Theorem Proving: A logical basis”, Fundamental Studies in Computer Science, North Holland,1978.Google Scholar
  20. [Mu]
    Musser D.L., “On Proving Inductive Properties of Abstract Data Types”, Proc. 7th POPL, Los Vegas, 1980.Google Scholar
  21. [Pa]
    Paulson L., “A Higher-Order Implementation of Rewriting”, Science of Computer Programming 3, 1983, pp 119–149.MathSciNetCrossRefzbMATHGoogle Scholar
  22. [Pl]
    Plaisted D.A., “A recursively defined ordering for proving termination of term rewriting systems”, U. of Illinois, Report n∘ R-78-943, 1978.Google Scholar
  23. [Re]
    Remy J.L. “Proving conditional identities by equational case reasoning rewriting and normalization”, Report 82-R-085, C.R.I.N., Nancy, 1982.Google Scholar
  24. [Sl]
    Slngle J.R., “Automated Theorem Proving for Theories with Simplifiers, Commutativity and associativity”, J.ACM 21:4, Oct 1974, pp 622–642.Google Scholar
  25. [St]
    Stickel M.E., “A unification algoritm for associative commutative functions” J.ACM 28:3, 1981, pp 423–434.CrossRefzbMATHGoogle Scholar
  26. [Th]
    Thiel J.J. “Un algorithme interactif pour l’obtention de definitions completes” Proc. 11th POPL, 1984.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • L. Fribourg
    • 1
  1. 1.Laboratoires de Marcoussis C.G.E.MarcoussisFrance

Personalised recommendations