Lógica de Programación: Clausulas, árboles y corrección de programas

Forma Skolem y Forma Clausal

Forma Skolem de una cláusula

(∀x₁)...(∀x_h) (A₁A₂...A_n ←B₁B₂...B_m) se escribe (∀x₁)...(∀x_h) ((B₁&B₂&..&B_m) → (A₁∨A₂∨...A_n)). Es equivalente a la fórmula: (∀x₁)...(∀x_h) (¬B₁∨¬B₂∨...∨¬B_m∨A₁∨A₂∨...A_n) denominada Forma Skolem. Cada forma Skolem determina una cláusula; las atómicas negadas se escriben a la derecha del símbolo ← y las no negadas a la izquierda. Las cláusulas o sus formas Skolem se pueden escribir sin cuantificadores; cada variable se sobreentiende cuantificada universalmente.

Método para obtener la Forma Clausal

1. Escribir la fórmula bien formada en su Forma Normal Prenex.
2. La forma sin cuantificar del paso 1 se escribe como conjunción de disyunciones; cada disyunción es un Skolem.
3. La eliminación de cuantificadores existenciales depende de si está precedido por cuantificadores universales. Si ningún universal precede al existencial, se sustituye su variable por una constante en todas sus subfórmulas y se elimina ese existencial. Si el existencial está precedido por uno o más cuantificadores universales, se sustituye su variable por una constante que tiene como subíndice las variables de los cuantificadores universales que precedían al existencial y se elimina ese existencial.
4. En la fórmula obtenida en el paso 3, se reemplaza cada disyunción Skolem por la cláusula que representa y se omiten los cuantificadores universales.
5. Se forma un sistema con las cláusulas obtenidas en el paso 4. Este sistema es la forma clausal de la forma clausurada de L_cp; las variables que intervienen se sobreentienden cuantificadas universalmente.

Árbol Clausal

Reglas de construcción de un árbol clausal

1. Se etiqueta la raíz con la cláusula. Se selecciona una fórmula atómica.
2. Se dibujan dos vástagos de la raíz: uno se etiqueta con una cláusula, el otro con una cláusula con las restantes fórmulas atómicas que permanecen en el mismo lugar del conectivo ←.
3. Se continúa el proceso indicado para la raíz para nodos clausales con más de una atómica.
4. El proceso finaliza cuando solo quedan nodos con cláusulas con solo una atómica (hojas del árbol).

Razonamientos Lógicos

Razonamiento y validez

Un razonamiento lógico es una sucesión finita de fórmulas bien formadas clausuradas (A₁∨A₂∨...∨A_n) del lenguaje L_cp. A₁, ..., A_n-1 son premisas y A_n es la conclusión. Un razonamiento {A₁, ..., A_n-1} ⊢ A_n es válido si de la verdad de las premisas resulta la verdad de la conclusión.

Razonamiento clausal y validez

Un razonamiento o argumentación clausal es una sucesión de cláusulas C₁, ..., C_n. Las k primeras cláusulas son premisas y el sistema de cláusulas C_k, ..., C_n es la conclusión. Un razonamiento clausal es válido si de las cláusulas premisas (que son aciertos) se deduce que las cláusulas conclusión también son aciertos.

Demostración no formal de razonamientos lógicos (árboles lógicos)

Método directo

Se suponen verdaderas las premisas {A₁, ..., A_n-1} del razonamiento {A₁, ..., A_n-1} ⊢ A_n y, si es válido, se llega a la verdad de la conclusión A_n.

Método de reducción al absurdo

Se etiqueta la raíz del árbol con la conjunción de premisas y la negación de la conclusión. Se desarrolla el árbol lógico con la técnica del método directo. Si el razonamiento es válido, todas las ramas del árbol se cierran con contradicciones (•).

Demostración formal de razonamientos clausales

Dado el razonamiento {C₁, ..., C_k-1} ⊢ C_k, ..., C_n, cada cláusula premisa C₁, ..., C_k-1 y cada cláusula D₁, ..., D_h que corresponden a la forma clausal de la negación lógica de la conclusión, es un acierto.

Método por refutación

Se etiqueta la raíz del árbol con las cláusulas premisas C₁, ..., C_k-1 y las cláusulas D₁, ..., D_h. Se desarrolla el árbol clausal. Si en una misma rama hay un vértice con cláusula X ← y otro con ← X, se cierra esa rama con (•), cláusula vacía.

Corrección de Programas

Programas correctos

Un programa S es correcto si, cuando se satisface la especificación {P} en el estado inicial de las variables y se ejecuta el programa, este termina en un estado final de las variables que satisface la postcondición {Q}. Si no se exige la premisa"termin", se dice que es parcialmente correcto; es totalmente correcto si efectivamente termina (no tiene bucles infinitos ni errores de ejecución).

Lógica de Hoare

Para la demostración formal de la corrección de un programa se utiliza la lógica de Hoare, que establece axiomas y reglas de inferencia para la demostración formal. Con la expresión {P}S{Q}, denominada terna o tripleta de Hoare, se representa la especificación funcional del programa S.

Fortalecimiento de la precondición y debilitamiento de la postcondición

Fortalecimiento de la precondición: Si {P} es una precondición y un conjunto de aserciones {P₀} verifica P₀ → P, se dice que {P₀} es un fortalecimiento de la precondición {P}.
Debilitamiento de la postcondición: El conjunto de aserciones {Q₀} es un debilitamiento de la postcondición {Q} si Q → Q₀.

Transformador de predicados

Dada la terna {P}S{Q}, para cada código o comando S, definimos la función transformador de predicados wp.S: Predicados → Predicados / {S, Q} ⊢ wp.S.Q. Como wp.S.Q se ha derivado del conjunto {S, Q}, la terna {wp.S.Q}S{Q} resulta correcta. Si además se prueba que {P → wp.S.Q} es verdadera, entonces wp.S.Q es la precondición P₀ más débil que hace correcta la terna {P}S{Q}. De la regla anterior resulta la regla del transformador de predicados: P → wp.S.Q / {P}S{Q}.