Jump to content

Encompassment ordering

Add links
From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by Jochen Burghardt (talk | contribs) at 12:57, 4 June 2014. The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

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.[1]

It is used e.g. in the Knuth-Bendix completion algorithm.

References

  1. ^ 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
Stub icon

This computer science article is a stub. You can help Wikipedia by expanding it.

Retrieved from "https://en.wikipedia.org/w/index.php?title=Encompassment_ordering&oldid=611522241"