Encompassment ordering
In theoretical computer science, in particular in automated theorem proving and term rewriting, the encompassment preorder on the set of terms, is defined by
- s≤t if a subterm of t is a substitution instance of s.
It is a preorder, i.e. reflexive and transitive, but not anti-symmetric,[note 1], nor total[note 2] [1] It is used e.g. in the Knuth-Bendix completion algorithm.
References
- ^ N. Dershowitz, J.-P. Jouannaud (1990). Jan van Leeuwen (ed.). Rewrite Systems. Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 243–320. Here:sect.2.1, p.250
 | This computer science article is a stub. You can help Wikipedia by expanding it. |
Cite error: There are <ref group=note> tags on this page, but the references will not show without a {{reflist|group=note}} template (see the help page).