Applications de l'Unification?

Question

Quelles sont les applications (pratiques) de Unification ? Lorsqu'il est en fait utilisé dans le monde réel?

Je ne pouvais pas comprendre l'idée de ce qu'il est vraiment et pourquoi il est considéré comme une partie de l'intelligence artificielle.

Answer 1

Unification est essentiellement un processus de substitution . Je l'ai vu appelé « correspondant à deux voies ».

En Prolog, dans d'autres langages de programmation logique et dans les langues directement basée sur la logique de réécriture ( Maude , Elan , etc ...) est le mécanisme par lequel des variables libres (logiques) sont lient aux conditions / valeurs. Dans Concurrent Prolog ces variables sont interprétées comme des canaux de communication.

OMI, la meilleure façon de le comprendre est avec quelques exemples de mathématiques (unification a été / est une base mécanisme clé, par exemple, dans le cadre de la recherche de démonstrateurs automatisé, un sous-domaine de l'IA, une autre utilisation dans de ). Les exemples qui suivent sont tirés du contexte de (CAS) :

Premier exemple:

donné un ensemble Q et deux opérations binaires * et + sur, puis * est à gauche distributive sur + si:

X * (Y + Z)   =   (X * Y) + (X * Z)   |1|

est règle de réécriture (un ensemble de règles de réécriture est un réécriture système ).

Si nous voulons appliquer cette règle de réécriture à un cas particulier, par exemple:

a * (1 + b)   |2|

Unify (via un algorithme d'unification) ce terme, | 2 |, avec côté gauche ( LHS ) de | 1 | et nous avons ce (trivial exprès) la substitution ( unificateur principal , mgu ):

{X/a, Y/1, Z/b}   |3|

, l'application | 3 | à la droite ( rhs ) de | 1 |, nous avons enfin:

(a * 1) + (a * b)

C'était simple et d'apprécier ce que l'unification peut faire, je vais montrer un petit exemple plus complexe.

Deuxième exemple:

Compte tenu de cette règle de réécriture:

log(X,Y) + log(X,Z)   =>   log(X,Y*Z)   |4|

nous appliquons à cette équation:

log(e,(x+1)) + log(e,(x-1)) = k   |5|

( LHS de | 5 | unifier LHS de | 4 |), nous avons donc cette mgu :

{X/e, Y/(x+1), Z/(x-1)}   |6|

Notez que X et x sont deux variables différentes. Ici, nous avons deux variables, X et Y, qui correspondent à deux termes composés , (x + 1) et (x-1), et non pas des valeurs simples ou variables.

Nous appliquons cette mgu , | 6 |, rhs de | 4 | alors et nous remettons cela à | 5 |; nous avons donc:

log(e,(x+1)*(x-1)) = k   |7|

et ainsi de suite.

(en espérant que je ne l'ai pas une erreur ou cela peut confondre encore plus néophyte.)

Answer 2

L'unification est un mécanisme clé . En pratique, l'unification dans ce contexte réduira considérablement l'usure de vos doigts.

Answer 3

Prolog , par exemple, utilise l'unification de trouver des valeurs pour les variables qui satisfont aux règles - voir cette explication pour un exemple. Je pense que c'est une technique typique dans les langages de programmation logiques en général, bien que je n'ai pas d'expérience avec les autres.

Answer 4

Unification est comme motif de correspondance, où l'on frotte ensemble deux structures, où les variables dans une sont autorisés à correspondre à des valeurs dans l'autre.

La forme la plus simple d'unification se produit chaque fois que vous appelez une fonction dans une langue normale. L'appelant a des arguments, et a des paramètres callee. Les paramètres sont « liés » aux arguments, et qui produit une instanciation de la fonction.

Une autre forme simple d'unification est lorsque vous utilisez une expression régulière pour la correspondance, par exemple à une commande que vous invite peut dire dir x*y*.z* qui correspondent à certains, mais pas tous les noms de fichiers.

Intelligence artificielle aime utiliser des moteurs d'inférence, pour tenter de simuler le raisonnement à partir d'un corpus de connaissances, généralement sous la forme de déclarations dans une logique. Pour choisir un exemple stupide, vous pourriez « savoir » que « tous les hommes sont mortels », comme dans forall(x)(man(x) implies mortal(x)). Ensuite, si vous posez une question « est Sam mortel » comme mortal(Sam)?, vous pouvez unifier que la règle pour obtenir une nouvelle question « est un homme Sam » man(Sam)?

L'espoir qui aide.