Reduction Orderings.

When we speak of an ordering we mean a total (or completable) reduction ordering. A reduction ordering is a well-founded ordering on ground terms that is compatible with contexts and is total or can be extended to a total such ordering. Reduction orderings are the basis for terminating computations by term rewriting. Saturate provides several classes of reduction orderings, including the lexicographic path ordering and its AC-variant. Orderings specify an orientation of binary atoms, in particular equalities, indicating the preferred direction when replacing equals by equals. A ordering $\succ$ also expresses preferences and directions of search when attempting to construct models for disjunctions: $A\vee B$ is to be viewed as $\neg B \to A$, if $A\succ B$, and this links ordered resolution to negation as failure in logic programming.

Imprint | Data Protection