Theory Path Orderings

  • Jürgen Stuber
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1631)


We introduce the notion of a theory path ordering (TPO), which simplifies the construction of term orderings for superposition theorem proving in algebraic theories. To achieve refutational completeness of such calculi we need total, E-compatible and E-antisymmetric simplification quasi-orderings. The construction of a TPO takes as its ingredients a status function for interpreted function symbols and a precedence that makes the interpreted function symbols minimal. The properties of the ordering then follow from related properties of the status function. Theory path orderings generalize associative path orderings.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. Baader, F. (1997). Combination of compatible reduction orderings that are total on ground terms. In 12th Ann. IEEE Symp. on Logic in Computer Science, Warsaw, pp. 2–13. IEEE Computer Society Press.Google Scholar
  2. Baader, F. and Nipkow, T. (1998). Term rewriting and all that. Cambridge University Press, Cambridge, UK.Google Scholar
  3. Bachmair, L. and Plaisted, D. (1985). Termination orderings for associativecommutative rewriting systems. Journal of Symbolic Computation 1: 329–349.zbMATHMathSciNetCrossRefGoogle Scholar
  4. Bachmair, L., Ganzinger, H. and Stuber, J. (1995). Combining algebra and universal algebra in first-order theorem proving: The case of commutative rings. In Proc. 10thWorkshop on Specification of Abstract Data Types, Santa Margherita, Italy, LNCS 906, pp. 1–29. Springer.CrossRefGoogle Scholar
  5. Delor, C. and Puel, L. (1993). Extension of the associative path ordering to a chain of associative commutative symbols. In Proc. 5th Int. Conf. on Rewriting Techniques and Applications, Montreal, LNCS 690, pp. 389–404. Springer.Google Scholar
  6. Dershowitz, N. and Hoot, C. (1995). Natural termination. Theoretical Computer Science 142: 179–207.zbMATHCrossRefMathSciNetGoogle Scholar
  7. Dershowitz, N. and Jouannaud, J.-P. (1990). Rewrite systems. In J. van Leeuwen (ed.), Handbook of Theoretical Computer Science: Formal Models and Semantics, Vol. B, chapter 6, pp. 243–320. Elsevier/MIT Press.Google Scholar
  8. Geser, A. (1996). An improved general path order. Applicable Algebra in Engineering, Communication and Computing 7: 469–511.zbMATHMathSciNetCrossRefGoogle Scholar
  9. Kapur, D. and Sivakumar, G. (1997). A total ground path ordering for proving termination of AC-rewrite systems. In Proc. 8th Int. Conf. on Rewriting Techniques and Applications, Sitges, Spain, LNCS 1103, pp. 142–156. Springer.Google Scholar
  10. March.
    e, C. (1996). Normalised rewriting: an alternative to rewriting modulo a set of equations. Journal of Symbolic Computation 21: 253–288.CrossRefMathSciNetGoogle Scholar
  11. Rubio, A. and Nieuwenhuis, R. (1995). A total AC-compatible ordering based on RPO. Theoretical Computer Science 142: 209–227.zbMATHCrossRefMathSciNetGoogle Scholar
  12. Stuber, J. (1998a). Superposition theorem proving for abelian groups represented as integer modules. Theoretical Computer Science 208(1-2): 149–177.zbMATHCrossRefMathSciNetGoogle Scholar
  13. Stuber, J. (1998b). Superposition theorem proving for commutative rings. In W. Bibel and P. H. Schmitt (eds), Automated Deduction-A Basis for Applications. Volume III. Applications, chapter 2, pp. 31–55. Kluwer, Dordrecht, The Netherlands.Google Scholar
  14. Waldmann, U. (1998). Extending reduction orderings to ACU-compatible reduction orderings. Information Processing Letters 67(1): 43–49.CrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Jürgen Stuber
    • 1
  1. 1.Max-Planck-Institut für InformatikSaarbrückenGermany

Personalised recommendations