theoretical computer science Theoretical computer science (TCS) is a subset of general computer science and mathematics that focuses on mathematical aspects of computer science such as the theory of computation, lambda calculus, and type theory. It is difficult to circumsc ...

, in particular in

automated theorem proving Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a maj ...

and

term rewriting In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. Such methods may be achieved by rewriting systems (also known as rewrite systems, rewrite engines, or reduc ...

, the containment, or encompassment,

preorder In mathematics, especially in order theory, a preorder or quasiorder is a binary relation that is reflexive and transitive. Preorders are more general than equivalence relations and (non-strict) partial orders, both of which are special c ...

(≤) on the set of

term Term may refer to: * Terminology, or term, a noun or compound word used in a specific context, in particular: **Technical term, part of the specialized vocabulary of a particular field, specifically: ***Scientific terminology, terms used by scient ...

s, is defined by :''s'' ≤ ''t'' if a

subterm In mathematical logic, a term denotes a mathematical object while a formula denotes a mathematical fact. In particular, terms appear as components of a formula. This is analogous to natural language, where a noun phrase refers to an object and a wh ...

of ''t'' is a

substitution instance Substitution is a fundamental concept in logic. A substitution is a syntactic transformation on formal expressions. To apply a substitution to an expression means to consistently replace its variable, or placeholder, symbols by other expressions. T ...

of ''s''. It is used e.g. in the

Knuth–Bendix completion algorithm The Knuth–Bendix completion algorithm (named after Donald Knuth and Peter Bendix) is a semi-decision algorithm for transforming a set of equations (over terms) into a confluent term rewriting system. When the algorithm succeeds, it effectively ...

Properties

* Encompassment is a

, i.e. reflexive and transitive, but not anti-symmetric,since both ''f''(''x'') ≤ ''f''(''y'') and ''f''(''y'') ≤ ''f''(''x'') for variable symbols ''x'', ''y'' and a

function symbol In formal logic and related branches of mathematics, a functional predicate, or function symbol, is a logical symbol that may be applied to an object term to produce another object term. Functional predicates are also sometimes called mappings, but ...

''f'' nor

total Total may refer to: Mathematics * Total, the summation of a set of numbers * Total order, a partial order without incomparable pairs * Total relation, which may also mean ** connected relation (a binary relation in which any two elements are comp ...

since neither ''a'' ≤ ''b'' nor ''b'' ≤ ''a'' for distinct constant symbols ''a'', ''b'' * The corresponding equivalence relation, defined by ''s'' ~ ''t'' if ''s'' ≤ ''t'' ≤ ''s'', is equality modulo renaming. * ''s'' ≤ ''t'' whenever ''s'' is a

of ''t''. * ''s'' ≤ ''t'' whenever ''t'' is a

of ''s''. * The union of any well-founded

rewrite order In theoretical computer science, in particular in automated reasoning about formal equations, reduction orderings are used to prevent endless loops. Rewrite orders, and, in turn, rewrite relations, are generalizations of this concept that have tur ...

''R''i.e. irreflexive, transitive, and well-founded binary relation ''R'' such that ''sRt'' implies ''u'' σ">Substitution_(logic)#First-order_logic.html" ;"title="/a>''s''Substitution (logic)#First-order logic">σsub>''p'' R ''u''[''t''σ]_''p'' for all terms ''s'', ''t'', ''u'', each path ''p'' of ''u'', and each Substitution (logic)#First-order logic, substitution ''σ'' with (<) is well-founded, where (<) denotes the

irreflexive kernel In mathematics, a binary relation ''R'' on a set ''X'' is reflexive if it relates every element of ''X'' to itself. An example of a reflexive relation is the relation " is equal to" on the set of real numbers, since every real number is equal to ...

of (≤).Dershowitz, Jouannaud (1990), sect.5.4, p. 278; somewhat sloppy, ''R'' is required to be a "terminating rewrite relation" there. In particular, (<) itself is well-founded.

Notes

References

Rewriting systems Order theory {{comp-sci-stub