4.8.1 La forma clausulada

4.8.1. La forma clausulada

Un literal es un átomo (es decir, un nombre de predicado con unos términos como argumentos entre paréntesis) o un átomo negado (o sea, con el símbolo «¬» delante). En el primer caso diremos que es un literal positivo, y, en el segundo, que es un literal negativo. Una cláusula es una sentencia de la forma:

L₁ $\/$ L₂ $\/$ ... $\/$ L_n

donde los L_i son literales con cualquier número de variables cada uno, y todas las variables están ligadas, es decir, las cláusulas son sentencias cerradas (Apartado 4.2.2).

Una sentencia está en forma clausulada si tiene la forma:

(L₁₁ $\/$ L₁₂ $\/$ ...) $/\$ (L₂₁ $\/$ L₂₂...) $/\$ ...

en la que cada cláusula (L_i1 $\/$ L_i2 $\/$ ...) tiene sus propias variables.

De una cláusula se dice también que es una colección de literales (implícitamente unidos por disyunciones), y de una sentencia en forma clausulada, que es una colección de cláusulas (implícitamente unidas por conjunciones).

Para toda sentencia cerrada de la lógica de predicados existe una sentencia equivalente en forma clausulada.

Las únicas diferencias con la lógica de proposiciones es que en lugar de variables proposicionales tenemos átomos, y que para pasar a forma clausulada la sentencia debe ser cerrada. Veremos que esto es así porque todas las variables que aparecen en una forma clausulada están cuantificadas universalmente.

El procedimiento para encontrar la sentencia equivalente en forma clausulada de una sentencia dada es un poco más largo.

DIT-ETSIT-UPM

Portada