|
Instantiation |
|
Description
One of the DP transformations is instantiation:
an SCC consisting of pairs P ∪ { s → t } over a set of rules R can be instantiated to
- (termination case)
P ∪ {sμ → tμ | μ = mgu(Ren(Cap(w)), s), v → w ∈ P} or to
P ∪ {sμ → tμ | μ = mgu(Ren(CapR-1(v)), t), v → w ∈ P}
- (innermost termination case)
P ∪ {sμ → tμ | μ = mgu(Capv(w), s), v → w ∈ P, sμ, vμ normal} or to
P ∪ {sμ → tμ | μ = mgu(Ren(CapU(t)-1(v)), t), v → w ∈ P, sμ normal}
Here, Ren(t) replaces all variables in t by different fresh variables and Cap(t) replaces all subterms with defined root
by a new variable. U(t) are the usable rules of t, and R-1 is the reversed system of R where all left- and
right-hand sides are exchanged. If a reversed system contains variables as left-hand sides, all symbols are called defined.
The first case for termination and innermost termination is called instantiation in AProVE whereas the second method
is called forward instantiation.
Application and Configuration
See the more general side about DP transformations.