Logica

Solo disponible en BuenasTareas
  • Páginas : 10 (2424 palabras )
  • Descarga(s) : 0
  • Publicado : 1 de diciembre de 2011
Leer documento completo
Vista previa del texto
Tema 2: Decidibilidad de la L´gica Cl´sica o a
Ingenier´ T´cnicas en Informatica de Gesti´n y Sistemas ıas e o Agust´ Valverde ın 27 de octubre de 2008

Decidibilidad de la L´gica Cl´sica Proposicional o a

­ Teorema: La L´gica Cl´sica Proposicional es decidible. o a ­ La construcci´n de las tablas de verdad constituyen un algoritmo de o demostraci´n autom´tica para esta l´gica. o a o ­ Lacomplejidad de todos los demostradores es exponencial en el peor de los casos

1

Algoritmo de Quine: interpretaciones parciales

J Es un m´todo de evaluaci´n de interpretaciones para una f´rmula mediante e o o interpretaciones parciales. J Una interpretaci´n parcial para una f´rmula fija el valor de algunas variables o o pero deja indefinidas otras: I(p) = 1 es una interpretaci´n parcial de p→ q. o J En algunos casos, se puede determinar el valor de una interpretaci´n parcial o sobre una f´rmula: Si J es la interpretaci´n tal que J(p) = 0, podemos o o afirmar que J(p → q) = 1, aunque J(q) est´ indefinido. e J Sin embargo: si I se define como I(p) = 1, no podemos determinar el valor de I(p → q).
2

Algoritmo de Quine
Œ El algoritmo construye un ´rbol binario donde cada rama seetiqueta con un a s´ ımbolo proposicional o su negaci´n y cada hoja con un valor de verdad. o  El conjunto de literales de cada rama (desde la ra´ a la hoja) determina una ız interpretaci´n parcial: la que hace verdaderos todos los literales. o Ž Las hojas se etiquetan con el valor de la f´rmula por la interpretaci´n parcial o o correspondiente a su rama.  Elegimos una ordenaci´n de las variables:[p1, p2, . . . , pn]. El primer ´rbol o a est´ formado por dos ramas etiquetadas con p1 y ¬p1; sucesivamente, este a primer ´rbol se extender´ seg´n la regla siguiente. a a u  Si alguna hoja no puede ser etiquetada, tomamos la siguiente variable, pn, y extendemos con dos ramas etiquetadas con pn y ¬pn. Terminamos, cuando todas las hojas est´n etiquetadas. a
3

Ejemplo: A = ((p ∧ q) → r) ∧ (p →q)) → (p → r)

p

¬p
1

q

¬q
1

r
1

¬r
1

4

Algoritmo de Quine: aplicaciones

J Una f´rmula es v´lida si y solo si todas las hojas se etiquetan con 1. o a J Una f´rmula es satisfacible si y solo si alguna hoja se etiquetan con 1. o J Una f´rmula es insatisfacible si y solo si todas las hojas se etiquetan con 0. o J Podemos estudiar igualmente la satisfacibilidad deconjuntos o la validez de inferencias: {A1, . . . , An} es satisfacible si y solo si A1 ∧ · · · ∧ An es satisfacible A1, . . . , An |= A si y solo si (A1 ∧ · · · ∧ An) → A es v´lida a A1, . . . , An |= A si y solo si A1 ∧ · · · ∧ An ∧ ¬A es insatisfacible
5

Principio de refutaci´n o
J Teorema: Si Ω es un conjunto de f´rmulas y A es otra f´rmula, entonce: o o Ω |= A si y solo si Ω ∪ {¬A} esinsatisfacible.

J Demostraci´n: o Ω |= A =⇒ Mod(Ω) ⊆ Mod(A) =⇒ Mod(Ω) ∩ Mod(A)c = ∅ =⇒ Mod(Ω) ∩ Mod(¬A) = ∅ =⇒ Mod(Ω ∪ {¬A}) = ∅ =⇒ Ω ∪ {¬A} es insatisfacible

6

Refutaci´n y deducci´n autom´tica o o a

J La mayor´ de los algoritmos de deducci´n autom´tica hacen uso del ıa o a principio de refutaci´n: o A1, . . . , An |= A si y solo si A1 ∧ · · · ∧ An ∧ ¬A es insatisfacible J Es decir, elprincipio de refutaci´n convierte el problema de generar y evaluar o modelos en un problema de b´squeda: ¿es posible encontrar una u interpretaci´n tal que I(A1 ∧ · · · ∧ An ∧ ¬A) = 1? o Equivalentemente: ¿Es posible encontrar una interpretaci´n tal que o I(A1 ∧ · · · ∧ An) = 1 e I(A) = 0?

7

Ejemplo: A = ((p ∧ q) → r) ∧ (p → q)) → (p → r)
Á Intentemos encontrar un contramodelo: → 0 ∧ 1 →1 ∧ p1 01 q1 r0 p1 →1 p 1 q1 →0 r0

Á La construcci´n del contramodelo conduce a una contradicci´n y por lo o o tanto, no existe ning´n contramodelo: A es v´lida u a

8

Ejemplo: A = ((p ∧ q) → r) ∧ (p → q)) → (p → r)
I((((p ∧ q) → r) ∧ (p → q)) → (p → r)) = 0 (1) I(((p ∧ q) → r) ∧ (p → q)) = 1 (2) I(p → r) = 0 (3) I((p ∧ q) → r) = 1 (4) I(p → q) = 1 (5) I(p) = 1 I(r) = 0 I(p ∧ q) = 0 (6)...
tracking img