Advertisement

Proof transformation for non-compatible rewriting

  • Reinhard Bündgen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1138)

Abstract

We present a new inference rule based characterization of abstract completion procedures. The completeness of this inference system is shown by proof transformation techniques using a very powerful new proof ordering. This new ordering improves over previously proposed orderings because (1) it can handle semi-compatible reduction relations and (2) it explains all known complete redundancy criteria in a uniform framework.

Keywords

Inference Rule Reduction Relation Elementary Proof Congruence Class Context Class 
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. 1.
    L. Bachmair and N. Dershowitz. Critical pair criteria for completion. Journal of Symbolic Computation, 6:1–18, 1988.Google Scholar
  2. 2.
    L. Bachmair and N. Dershowitz. Equational inference, canonical proofs, and proof orderings. Journal of the ACM, 41(2):236–216, 1994.CrossRefGoogle Scholar
  3. 3.
    B. Benninghofen, S. Kemmerich, and M. M. Richter. Systems of Reductions. Springer-Verlag, 1987.Google Scholar
  4. 4.
    G. M. Bergman. The diamond lemma for ring theory. Advances in Mathematics, 29:178–218, 1978.Google Scholar
  5. 5.
    B. Buchberger. Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal. PhD thesis, Universität Innsbruck, 1965.Google Scholar
  6. 6.
    R. Bündgen. Abstract completion for non-compatible rewrite relations. Technical Report 96-13, Wilhelm-Schickard-Institut, Universität Tübingen, D-72076 Tübingen, 1996.Google Scholar
  7. 7.
    R. Bündgen. Buchberger's algorithm: the term rewriter's point of view. Theoretical Computer Science, 1996 (to appear).Google Scholar
  8. 8.
    R. Bündgen. Symmetrization based completion. In Proceeding on Conference on Symbolic Rewriting Techniques, 1996. (submitted, presented at SRT'95, Monte Verita, CH, May 1995).Google Scholar
  9. 9.
    N. Dershowitz and Z. Manna. Proving termination with multiset orderings. Commun. ACM, 22(8):465–476, 1979.Google Scholar
  10. 10.
    H. Ganzinger. Completion with history-dependent complexities for generated equations. In Sannellla and Tarlecki, editors, Recent Trends in Data Type Specification, 1987.Google Scholar
  11. 11.
    D. E. Knuth and P. B. Bendix. Simple word problems in universal algebra. In Leech, editor, Computational Problems in Abstract Algebra. Pergamon Press, 1970.Google Scholar
  12. 12.
    W. Küchlin, Inductive completion by ground proof transformation. In Aït-Kaci and Nivat, editors, Rewriting Techniques, volume 2 of Resolution of Equations in Algebraic Structures. Academic Press, 1989.Google Scholar
  13. 13.
    P. Le Chenadec. Canonical Forms in Finitely Presented Algebras. Pitman, London, 1986.Google Scholar
  14. 14.
    C. Marché. Normalised rewriting and normalised completion. In Ninth Anual Symposium on Logic in Computer Science. IEEE Computer Society Press, 1994.Google Scholar
  15. 15.
    M. H. A. Newman. On theories with a combinatorial definition of “equivalence”. Annals of Mathematics, 43(2):223–243, 1942.Google Scholar
  16. 16.
    L. Pottier. Algorithmes de complétion et généralison en logique du premier ordre. PhD thesis, Université Nice-Sophia Antipolis, Parc Valrose, Fac. Sciences, F-06034 Nice, 1989.Google Scholar
  17. 17.
    F. Winkler and B. Buchberger. A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm. In Proc. Colloquium on Algebra, Combinatorics and Logic in Computer Science. J. Bolyai Math. Soc., J. Bolyai Math. Soc. and North-Holland, 1985.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1996

Authors and Affiliations

  • Reinhard Bündgen
    • 1
  1. 1.Wilhelm-Schickard-InstitutUniversität TübingenTübingen

Personalised recommendations