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.

...