Theory Path Orderings
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.
- 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
- Baader, F. and Nipkow, T. (1998). Term rewriting and all that. Cambridge University Press, Cambridge, UK.Google Scholar
- 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
- 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
- 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
- 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