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.