se trata de una regla o mecanismo de inferencia utilizada por la mayoría de los sistemas de programación lógica, sobre cierto tipo de proposiciones, especialmente para los demostradores automatizados de teoremas.
(Wikipedia).
La programación se relaciona con el uso de la lógica (restringida a cláusulas) para representar y resolver problemas. Este uso es ampliamente aceptado en el ámbito de la inteligencia artificial (IA), donde la idea se resume como sigue: un problema o sujeto de investigación puede describirse mediante un conjunto de fbfs, de preferencia en forma de cláusulas. Si tal descripción es lo suficientemente precisa, la solución al problema o la respuesta a la pregunta planteada en la investigación, es una consecuencia lógica del conjunto de fbfs que describen el problema.
Por lo tanto, encontrar que fbf 𝛷 son consecuencia lógica de un conjunto de fbf 𝛥, es crucial para muchas áreas de la IA, incluyendo la programación lógica. De forma que se busca un procedimiento, algorítmico, que nos permita establecer si 𝛥 ⊨ 𝛷 es el caso, o no.
En el caso de la lógica proposicional, la implicación lógica es decidible, es decir, existe un algoritmo que puede resolver el problema (contestar si ó no para cada caso particular 𝛥 ⊨ 𝛷). Si n es el número de átomos distintos que ocurren en estas fbf, el número de interpretaciones posibles es finito, de hecho es 2ⁿ. Un algoritmo para computar 𝛥 ⊨ 𝛷 simplemente busca si 𝛷 es verdadero en todos los modelos de 𝛥.
En el contexto de la lógica de primer orden, intuitivamente, vemos que el procedimiento de decisión de la lógica proposicional no es adecuado, pues en este caso podemos tener una cantidad infinita de dominios e interpretaciones diferentes.
(Alejandro Guerra Hernández, Departamento de Inteligencia Artificial, Universidad Veracruzana, México)
Ver articulo completo aquí.