Pourquoi l'unification est-elle si importante pour déduire les moteurs?

^{J'apprends moi-même la vérification automatisée de théorèmes / les solveurs SMT / assistants de vérification et je poste une série de questions sur le processus, en commençant ici .}

Je continue de lire sur l' algorithme d'unification .

• Qu'est-ce que c'est et pourquoi est-il si important pour les moteurs d'inférence ?
• Pourquoi est-ce si important pour l'informatique?

L'unification est un concept si fondamental en informatique que peut-être même à un moment donné, nous le tenons pour acquis. Chaque fois que nous avons une règle ou une équation ou un modèle et que nous voulons l'appliquer à certaines données, l'unification est utilisée pour spécialiser la règle aux données. Ou si nous voulons combiner deux règles générales mais qui se chevauchent, l'unification nous fournit la règle combinée la plus générale. L'unification est au cœur de

• Les prouveurs de théorèmes et assistants de preuve, incluent certains basés sur une unification d'ordre supérieur.
• Implémentations de Prolog (en tant que résolution).
• Tapez des algorithmes d'inférence.
• Linguistique informatique / traitement du langage naturel.
• Des systèmes de réécriture de termes tels que Maude, qui peuvent être utilisés comme base de la sémantique du langage de programmation.
• Bases de données déductives.
• Systèmes experts ou plus généralement Intelligence artificielle.
• Systèmes d'algèbre informatique.
• Correspondance de modèles dans les langages fonctionnels (au moins en partie ... correspondance uniquement).
• Quelques approches d'analyse.
• Certains langages de requête, notamment impliquant le Web sémantique.

Les assistants de preuve comme Isabelle / HOL travaillent au niveau syntaxique sur un calcul logique. Imaginez que vous ayez la règle du modus ponens (MP)

$\qquad \displaystyle P\to Q, P\ \Longrightarrow\ Q$

et l'objectif de preuve

$\qquad \displaystyle (a \lor b) \to (c \land d), a \lor b \ \overset{!}{\Longrightarrow} c\land d$

Nous, les humains, voyons immédiatement que cela suit avec le modus ponens, mais la machine doit correspondre à l'objectif de gouverner syntaxiquement (que vous le fassiez apply rule mpou non apply simp), et c'est ce que fait l'unification. L'algorithme trouve avec φ ( P ) = a ∨ b et φ ( Q ) = c ∧ d , instancie la règle et l'applique.$\varphi$$\varphi(P) = a\lor b$$\varphi(Q) = c \land d$

La bonne chose à propos des méthodes des assistants comme simpmaintenant est que si votre objectif est

$\qquad \displaystyle (a \lor b) \to (c \land d), a \ \overset{!}{\Longrightarrow} d$

$P \land Q \Longrightarrow P$$P \Longrightarrow P \lor Q$

$\Gamma = \{\varphi_1, \dots, \varphi_n\}$

$\qquad \Gamma \Longrightarrow \psi$

signifie ce qui suit:

$\Gamma$$\psi$

$\Gamma \Longrightarrow \psi$$\psi$

$P$$Q$$\varphi$

$\models$$\Longrightarrow$

Je ne pense pas qu'il soit important d' inférer des moteurs . L'algorithme d'unification est cependant très utile pour l' inférence de type . Il s'agit de deux types d'inférence très différents.

L'inférence de type est importante pour l'informatique car les types sont importants dans la théorie des langages de programmation, qui est une partie importante de l'informatique. Les types sont également proches de la logique et sont intensivement utilisés dans la démonstration automatisée des théorèmes. Il existe des implémentations d'algorithmes d'unification dans de nombreux, sinon tous, assistants de preuve et solveurs SMT.

Les moteurs d'inférence sont liés à l'intelligence artificielle, qui est également importante mais très différente. (J'ai vu des liens entre l'apprentissage et la logique, mais cela semble tiré par les cheveux.)