3.8.6 Cláusulas de Horn

3.8.6. Cláusulas de Horn

Antes de explicar lo que son las cláusulas de Horn nos detendremos un momento en la escritura de cláusulas en forma de condicional, que ayuda a comprender su significado.

La forma clausulada es interesante, como hemos visto, para la implementación de sistemas deductivos, pero su interpretación por la mente humana es difícil. Sin embargo, podemos hacer una transformación inversa muy sencilla que ayuda a interpretar las cláusulas. Dada una cláusula cualquiera, L₁ $\/$ L₂ $\/$ ..., podemos transformarla en una sentencia equivalente con forma de condicional. Para ello, escribimos primero los literales negativos y luego los positivos:

¬p₁ $\/$ ¬p₂ $\/$ ... $\/$ ¬p_k $\/$ q₁ $\/$ q₂ $\/$ ... $\/$ q_m

Por una de las leyes de de Morgan (la equivalencia (3) del Apartado 3.4.2), esta sentencia es equivalente a:

¬(p₁ $/\$ p₂ $/\$ ... $/\$ p_k) $\/$ q₁ $\/$ q₂ $\/$ ... $\/$ q_m

y por la equivalencia (9) esta otra sentencia también es equivalente:

(p₁ $/\$ p₂ $/\$ ... $/\$ p_k) (q₁ $\/$ q₂ $\/$ ... $\/$ q_m)

Se llaman cláusulas de Horn aquellas que tienen como máximo un literal positivo. Hay dos tipos:

Las cláusulas determinadas (definite clauses), o «cláusulas de Horn con cabeza» son las que sólo tienen un literal positivo:
(¬p₁ $\/$ ¬p₂ $\/$ ... $\/$ ¬p_k $\/$ q) (p₁ $/\$ p₂ $/\$ ... $/\$ p_k q)
Caso particular son las no tienen más que ese literal positivo, que representan «hechos» , es decir, conocimiento factual.
Los objetivos determinados (definite goals), o «cláusulas de Horn sin cabeza» son las que no tienen ningún literal positivo:
(¬p₁ $\/$ ¬p₂ $\/$ ... $\/$ ¬p_k) ¬(p₁ $/\$ p₂ $/\$ ... $/\$ p_k)
En este caso, las fórmulas atómicas p₁,p₂,...,p_k son inconsistentes, es decir no es posible que sean todas verdaderas. Provienen de la negación de conclusiones que el sistema deductivo debe obtener mediante resolución y refutación.

Además de permitir la implementación de sistemas deductivos completos, una propiedad interesante de las cláusulas de Horn es que la asunción del mundo cerrado no conduce a una teoría inconsistente (Apartado 3.5.1), según este teorema:

«Si ₀ está formada por cláusulas de Horn que no son inconsistentes entonces la teoría que resulta de la asunción del mundo cerrado, T_D, es consistente»

El interés de las cláusulas de Horn (como el de los demás conceptos introducidos en este Capítulo) está en su versión de lógica de predicados, donde también es aplicable el teorema anterior, y donde son el fundamento de la programación lógica.

DIT-ETSIT-UPM

Portada