¿Por qué la unificación es tan importante para los motores de inferencia?

^{Estoy aprendiendo Pruebas automatizadas de teoremas / Solucionadores SMT / Asistentes de pruebas por mí mismo y publico una serie de preguntas sobre el proceso, comenzando aquí .}

Sigo leyendo sobre el algoritmo de unificación .

• Qué es y por qué es tan importante motores de inferencia ?
• ¿Por qué es tan importante para la informática?

La unificación es un concepto tan fundamental en ciencias de la computación que quizás a veces incluso lo damos por sentado. Cada vez que tenemos una regla o ecuación o patrón y queremos aplicarlo a algunos datos, la unificación se utiliza para especializar la regla a los datos. O si queremos combinar dos reglas generales pero superpuestas, la unificación nos proporciona la regla combinada más general. La unificación es el núcleo de

• Los probadores de teoremas y asistentes de pruebas, incluyen algunos basados ​​en la unificación de orden superior.
• Prolog implementaciones (como resolución).
• Algoritmos de inferencia de tipo.
• Lingüística computacional / procesamiento del lenguaje natural.
• Sistemas de reescritura de términos como Maude, que pueden utilizarse como base de la semántica del lenguaje de programación.
• Bases de datos deductivas.
• Sistemas expertos o, más en general, inteligencia artificial.
• Sistemas de álgebra computacional.
• Coincidencia de patrones en lenguajes funcionales (al menos en parte ... solo coincidencia).
• Algunos enfoques de análisis.
• Algunos lenguajes de consulta, especialmente relacionados con la Web Semántica.

Asistentes de prueba como Isabelle / HOL trabajan a nivel sintáctico en un cálculo lógico. Imagina que tienes la regla modus ponens (MP)

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

y el objetivo de la prueba

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

apply rule mpapply simp$\varphi$$\varphi(P) = a\lor b$$\varphi(Q) = c \land d$

Lo bueno de los métodos de los asistentes como simpahora es que si su objetivo es

$\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$

significa lo siguiente:

$\Gamma$$\psi$

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

$P$$Q$$\varphi$

$\models$$\Longrightarrow$

No creo que sea importante inferenciar motores . Sin embargo, el algoritmo de unificación es muy útil para inferencia de tipos . Estos son dos tipos muy diferentes de inferencia.

La inferencia de tipos es importante para la informática porque tipos son importantes en la teoría de los lenguajes de programación, que es una parte importante de la informática. Los tipos también están cerca de la lógica y se usan intensivamente en la demostración automatizada de teoremas. Hay implementaciones de algoritmos de unificación en muchos, si no todos, asistentes de prueba y solucionadores SMT.

Los motores de inferencia están relacionados con la inteligencia artificial, que también es importante pero muy diferente. (He visto vínculos entre aprendizaje y lógica, pero esto parece descabellado).