Unification
المؤلف:
Chang, C.-L. and Lee, R. C.-T.
المصدر:
Symbolic Logic and Mechanical Theorem Proving. New York: Academic Press, 1997.
الجزء والصفحة:
...
10-2-2022
1201
Unification
Consider expressions built up from variables and constants using function symbols. If 
, ..., 
are variables and 
, ..., 
are expressions, then a set of mappings between variables and expressions ![<span style=]()
{t_1|v_1,...,t_n|v_n}" src="https://mathworld.wolfram.com/images/equations/Unification/Inline5.svg" style="height:24px; width:140px" /> is called a substitution.
If ![eta=<span style=]()
{t_1|v_1,...,t_n|v_n}" src="https://mathworld.wolfram.com/images/equations/Unification/Inline6.svg" style="height:24px; width:173px" /> and 
is an expression, then 
is called an instance of 
if it is received from 
by simultaneously replacing all occurrences of 
(for 
) by the respective 
.
If ![eta=<span style=]()
{t_1|v_1,...,t_n|v_n}" src="https://mathworld.wolfram.com/images/equations/Unification/Inline14.svg" style="height:24px; width:173px" /> and ![theta=<span style=]()
{u_1|x_1,...,u_n|x_m}" src="https://mathworld.wolfram.com/images/equations/Unification/Inline15.svg" style="height:24px; width:185px" /> are two substitutions, then the composition of 
and 
(denoted 
) is obtained from ![<span style=]()
{t_1theta|v_1,...,t_ntheta|v_n,u_1|x_1,...,u_n|x_m}" src="https://mathworld.wolfram.com/images/equations/Unification/Inline19.svg" style="height:24px; width:314px" /> by removing all elements 
such that 
and all elements 
such that 
is one of 
, ..., 
.
A substitution 
is called a unifier for the set of expressions ![<span style=]()
{E_1,...,E_n}" src="https://mathworld.wolfram.com/images/equations/Unification/Inline27.svg" style="height:22px; width:92px" /> if 
. A unifier 
for the set of expressions ![<span style=]()
{E_1,...,E_n}" src="https://mathworld.wolfram.com/images/equations/Unification/Inline30.svg" style="height:22px; width:92px" /> is called the most general unifier if, for any other unifier for the same set of expressions 
, there is yet another unifier 
such that 
.
A unification algorithm takes a set of expressions as its input. If this set is not unifiable, the algorithm terminates and yields a negative result. If there exists a unifier for the input set of expressions, the algorithm yields the most general unifier for this set of expressions. The unification algorithm serves as a tool for the resolution principle. It is also a basis for term rewriting systems.
REFERENCES
Chang, C.-L. and Lee, R. C.-T. Symbolic Logic and Mechanical Theorem Proving. New York: Academic Press, 1997.
الاكثر قراءة في المنطق
اخر الاخبار
اخبار العتبة العباسية المقدسة
