Ingenieria de softwarе

[pic 1]

Proyecto Final Lógica II semestre - 2019

Manual de usuario

Tabla de contenido

Objetivo del documento3

Principio de funcionamiento del método  3

Requerimientos de la aplicación 6

Manual de usuario 7

Pantalla Inicial5

Ingreso de Formulas6                                                Resultados……..………………………………………………………………………………………………………………7

Referencias y Bibliografía……………………………………………………………………………………………… 13                      

1. Objetivo del documento

El objetivo principal de este documento es indicar el uso adecuado de la aplicación. A través del mismo, el usuario puede contextualizar la verificación de satisfacibilidad utilizando el “Método de resolución”.

1. Principio de funcionamiento del método

• Resolución proposicional:

El método de resolución es un algoritmo propuesto por J.A. Robinson en 1965. La entrada del algoritmo no es una fórmula, sino un conjunto de cláusulas y el algoritmo determina si son insatisfacibles [1].

Este método como tal se utiliza para interpretar la deducción y solamente para clausulas.

• Formas normal conjuntiva y disyuntiva:

Una formula proposicional está en forma normal cuando únicamente está constituida de disyunciones o conjunciones, y la negación solo afecta a los literales, es decir en ella no existen operadores booleanos condicionales, bi-condicionales, ni negación de la fórmula [2]

Una forma normal puede estar en forma normal disyuntiva o forma normal conjuntiva.

Una fórmula está en Forma Normal Disyuntiva (FND) si está constituida por una disyunción de conjunciones, es decir el operador principal es la disyunción y las conjunciones son las dependientes.

Donde C1 ∨ C2 ∨ C3 ∨ C4 ∨ ...Cn, y cada Ci una cláusula y Bi1 ∨ Bi2 ∨ Bi3 ∨ ...Bin, es un literal de la cláusula.

Son ejemplos de FND las siguientes expresiones:

p ∨ q

(¬p ∧ ¬q ∧ r) ∨ (p ∧ s)

(q ∧ p) ∨ (¬p) ∨ (q)

¬p

Las siguientes formulas no están en FND:

¬ (p ∨ s) (el operador de negación afecta la fórmula)

((¬p ∨ q ∨ s) ∧ r)) ∨ ¬s (tiene una disyunción)

Una formula está ́a en Forma Normal Conjuntiva (FNC) si está constituida por una conjunción de disyunciones, es decir el operador principal es la conjunción y las disyunciones son las dependientes.

Donde C1 ∧ C2 ∧ C3 ∧ C4 ∧ ...Cn, y cada Ci una cláusula y Bi1 ∧ Bi2 ∧ Bi3 ∧ ...Bin, es un literal de la cláusula.

Son ejemplos de FNC las siguientes expresiones:

¬p ∧ s

(p ∨ q) ∧ (p ∨ ¬s)

(¬p ∨ ¬q ∨ ¬s) ∧ (p ∨ s) ∧ (¬p)

Q

Las siguientes formulas no están en forma normal conjuntiva FCN

¬ (p ∧ s) (el operador de negación afecta la fórmula)

((¬p ∧ q) ∨ ¬r)) ∧ (¬p) (tiene una disyunción en la fórmula).

Una fórmula en FND será insatisfacible si todas sus disyunciones son falsas, de lo contrario, se debe establecer si es una tautología o una fórmula satisfacible.

Una fórmula en FNC será una tautología si, todas sus conjunciones son verdaderas, de lo contrario, se debe establecer si la fórmula es satisfacible o insatisfacible.

Toda fórmula proposicional tiene su equivalente en FNC.

Para convertir una fórmula a FNC, es posible establecer una serie de pasos, los cuales garantizan la propiedad de equivalencia lógica.

• Eliminar todos los conectivos diferentes a: negación, conjunción y disyunción. (se eliminan los operadores ↔ y →).
• Aplicar las leyes de De Morgan, para llevar todas las apariciones de ¬ hasta los átomos.

¬ (A ∧ B) ↔ (¬A ∨ ¬B)

¬ (A ∨ B) ↔ (¬A ∧ ¬B)

• Eliminar las dobles negaciones.
• Aplicar de forma repetida las leyes Distributivas, para llevar todas las apariciones de ∨ hasta los átomos.

A ∨ (B ∧ C) ↔ (A ∨ B) ∧ (A ∨ C)

(A ∧ B) ∨ C ↔ (A ∨ C) ∧ (B ∨ C)

Literales, cláusulas y Forma clausal

Un literal es una proposición atómica p su negación ¬p, es decir una variable proposicional o la negación de una variable proposicional. Todo literal tiene un complemento. Si s es un literal, ¬s es su complemento. Si ¬s es un literal, entonces s es su complemento. Los literales se constituyen las clausulas.

Una cláusula se compone de literales que se encuentran unidos por medio del operador de disyunción, esta disyunción se puede dar entre cero o más literales. Una cláusula es una disyunción de literales.

Una cláusula que no contenga literales se denomina vacía, y su representación es mediante el símbolo #. Una cláusula vacía es insatisfacible.

Una fórmula está en Forma Clausal si está conformada exclusivamente por un conjunto de cláusulas [2].

[pic 2]

Imagen 1. Formulas proposicionales

La transformación de una fórmula en FNC a Forma Clausal es inmediata sustituyendo las conectivas ∧ por comas y englobando las disyunciones entre llaves.

Algunos aspectos para destacar en los conjuntos de cláusulas son:

• Existen clausulas con un solo literal, a las cuales se les conoce como cláusulas unitarias.
• Cuando un literal se repite en la cláusula es posible aplicarla equivalencia lógica (p ∨ p) ⇔ p. En este caso la cláusula no pierde sus propiedades.
• Cuando una cláusula no contiene ningún literal, se denomina clausula vacía y como se ha mencionado, es insatisfacible y no puede ser satisfecha.
• Una cláusula que tiene un literal verdadero, se denomina cláusula de Horn.

Método de resolución

El método de resolución es un procedimiento automático es un método que trabaja únicamente con cláusulas que estén en FNC. En este método se aplica una única regla de inferencia, denominada regla de resolución.

La regla de resolución se aplica cuando existan literales complementarios entre pares de cláusulas [3].

Cuando en dos cláusulas C1 y C2, se contenga en cada una literales tales que l ∈ C1 y ¬l ∈ C2, se afirma que son clausulas resolubles. El resolvente entre dos clàusulas C1 y C2, da lugar a una nueva clausula C.

El resolvente entre C1 y C2, da lugar a una nueva cláusula respecto al literal l. A este proceso se le denomina paso de resolución. La aplicación del resolvente se denota de la siguiente manera:

Rl(C1, C2)=(C1– {l}) ∪ (C2– {¬l})

Por ejemplo, si se tienen las cláusulas:

C1 = pq¬r y C2 = qr¬t

el literal c, está en la cláusula C1 = ¬r y en la cláusula C2 = r.

El resolvente entre C1 y C2, se obtienen de la siguiente manera:

R(C1, C2)=(pq¬r– {¬r}) ∪ (qr¬t– {r}) = pq ∪ q¬t = pq¬t

Los siguientes son ejemplos en los cuales se aplica el resolvente a dos clausulas:

...