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 {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 {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 {t_1|v_1,...,t_n|v_n}" src="https://mathworld.wolfram.com/images/equations/Unification/Inline14.svg" style="height:24px; width:173px" /> and {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 {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 {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 {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.

اخر الاخبار

اخبار العتبة العباسية المقدسة

أساتذة المجمَع العلمي يشرفون على تحكيم المسابقة القرآنية في جامعة النهرين

قسم الشؤون الدينية ينشر صناديق مخصصة لزكاة الفطرة داخل مرقد أبي الفضل العباس (عليه السلام) وخارجه

شعبة التوجيه الديني النسوي تختتم مجالسها العبادية لإحياء ليالي القدر المباركة

قسم الشؤون الفكرية ينظم ندوة توعوية ثقافية في محافظة ذي قار

المزيد

الآخبار الصحية

تأثير اللياقة البدنية على الدماغ

تجربة سريرية تظهر فوائد اللوز للمصابين بالسمنة

اكتشاف طريقة غير متوقعة لتقليل خطر الإصابة بالسكري

خمسة مؤشرات صحية مهملة قد تنقذ حياتك

المزيد

الآخبار التكنلوجية

علماء الجيولوجيا يفكون لغز الصدع العملاق تحت الماء في المحيط الأطلسي

تحذير جديد: الاحترار العالمي يتسارع وقد نكسر حاجز 1.5 درجة قبل 2030

الصين تكشف عن ألياف كربون تفوق قوة الفولاذ بـ10 مرات

الجهاز المناعي يظهر دورا غير متوقع في صحة العظام

المزيد

مواضيع ذات صلة

Lemma

Proof

Zeno,s Paradoxes

Unexpected Hanging Paradox

Strange Loop

Sorites Paradox

Simpson,s Paradox

Russell,s Antinomy

Paradox

Newcomb,s Paradox

Missing Dollar Paradox

Line Point Picking