The simplest algorithm for unication  that is taught in many introductory courses in AI:

Write down two terms and set markers (e.g., two index fingers) at the beginning of the terms.

This simple algorithm methodically finds disagreements in the two terms to be unfied, and attempts to repair them by binding variables to terms: it fails when function symbols clash, or when an attempt is made to unify a variable with a term containing that variable (which is impossible)

Then:

1. Move the markers together, one symbol at a time, until both move at the end of the term (success!), or until they point to two different symbol

2. If the two symbols are both non-variables, then fail;

 otherwise, one is a variable (call it x) and the other is the rest symbol of a subterm (call it t):

 (a) If x occurs in t, then fail;

(b) Otherwise, write down x -> t" as part of the solution, replace x everywhere by t (including in the solution), and return to (1).

آخر تعديل: الاثنين، 22 مايو 2023، 4:18 PM