Subsumption lattice: Difference between revisions
No edit summary |
No edit summary |
||
| Line 1: | Line 1: | ||
{{AFC submission|||ts=20120818162457|u=93.220.96.124|ns=5}} |
{{AFC submission|||ts=20120818162457|u=93.220.96.124|ns=5}} |
||
A '''Subsumption lattice''' is a mathematical structure used in theoretical background of [[Theorem_proving|automated theorem proving]] and other [[Symbolic_computation|symbolic computation]] applications. |
|||
==Definition== |
==Definition== |
||
A [[Term (logic)|term]] ''t<sub>1</sub>'' is said to '''subsume''' a term ''t<sub>2</sub>'' if a [[Unification_(computer_science)#Substitution|substitution]] ''s'' exists such that ''s'' applied to ''t<sub>1</sub>'' yields ''t2''. In this case, ''t1'' is also called '''more general than''' ''t<sub>2</sub>'', and ''t<sub>2</sub>'' is called '''more specific than''' ''t<sub>1</sub>''. |
A [[Term (logic)|term]] ''t<sub>1</sub>'' is said to '''subsume''' a term ''t<sub>2</sub>'' if a [[Unification_(computer_science)#Substitution|substitution]] ''s'' exists such that ''s'' applied to ''t<sub>1</sub>'' yields ''t2''. In this case, ''t1'' is also called '''more general than''' ''t<sub>2</sub>'', and ''t<sub>2</sub>'' is called '''more specific than''' ''t<sub>1</sub>''. |
||
Revision as of 10:28, 19 August 2012
 | This article, Subsumption lattice, has recently been created via the Articles for creation process. Please check to see if the reviewer has accidentally left this template after accepting the draft and take appropriate action as necessary.
Reviewer tools: Inform author |
A Subsumption lattice is a mathematical structure used in theoretical background of automated theorem proving and other symbolic computation applications.
Definition
A term t1 is said to subsume a term t2 if a substitution s exists such that s applied to t1 yields t2. In this case, t1 is also called more general than t2, and t2 is called more specific than t1.
The set of all terms over a given signature can be made a lattice over the partial ordering relation "... is more specific than ..." as follows:
- two terms are considered equal if they differ only in their variable namings,
- an artificial minimal element Ω ("the overspecified term") is added, which is considered to be more specific than any other term.
This lattice is called the subsumption lattice.
Properties
The join and the meet operation in this lattice are called anti-unification and unification, respectively. A variable x and the artificial element Ω is the top and the bottom element of the lattice, respectively. Each ground term is an atom of the lattice.
If f and g is a binary and unary function symbol, respectively, and x and y denote variables, then the terms f(x,y), f(x,x), f(g(x),g(x)), f(g(x),y), and f(g(x),g(y)) form the minimal non-modular lattice N5; its appearance prevents the subsumption lattice from being modular and hence also from being distributive. Non-modular sublattice N5 in subsumption lattice
Origin
Apparently, the subsumption lattice has first been investigated by Gordon D. Plotkin in 1970[1].