A.5.2 El sistema deductivo de Prolog

A.5.2. El sistema deductivo de Prolog

Si recordamos el modelo procesal básico de Prolog descrito en el Apartado A.3, podemos ahora decir que hace uso de dos reglas de inferencia:

la de particularización de un universal (cuando sustituye variables por constantes buscando unificaciones) y
la de modus ponens (cuando unifica un subobjetivo «A» con la cabeza de una regla «A:-B,C...» )

Con la restricción sintáctica de que sólo se admitan cláusulas de Horn en el lenguaje, y con la restricción en la búsqueda de que toda transición de un estado al siguiente se realiza unificando el subobjetivo en curso (un literal positivo) con una regla o con un hecho (apartado A.3.1), modus ponens es equivalente a resolución con refutación. En efecto, unificar el objetivo «A» con la cabeza de la regla «A:-B,C...» (y obtener los subobjetivos «B, C,...» es lo mismo que es resolver la cláusula «A $\/$ ¬B $\/$ ¬C...» con «¬A» y obtener la resolvente «¬B $\/$ ¬C...» (que es lo mismo que «¬(A $/\$ B $/\$ C...)» ).

Por tanto, se aplica una estrategia de «resolución lineal con la entrada» (Apartado 3.8.6) que, con sólo cláusulas de Horn, permite que el sistema deductivo sea completo. En realidad, la compleción en el sistema deductivo de Prolog sólo se pierde por el hecho de realizar una búsqueda en profundidad, como hemos visto en el Apartado A.3.3.

Una descripción detallada del modelo procesal de Prolog puede encontrarse en el libro de Maier y Warren (1988) [61].

DIT-ETSIT-UPM

Portada