Logica Modal
-
Upload
lexleo1000 -
Category
Documents
-
view
36 -
download
0
Transcript of Logica Modal
Introducción a la Lógica Modal
Pedro Cabalar
Depto. ComputaciónUniversidade da Coruña, SPAIN
4 de mayo de 2006
P. Cabalar ( Depto. Computación Universidade da Coruña, SPAIN )Lógica Modal 4 de mayo de 2006 1 / 14
Outline
1 Introducción
2 Modal proposicional: sintaxis y axiomatizaciónSintaxisAxiomatización
3 Semántica. Marcos de Kripke
P. Cabalar ( Depto. Computación Universidade da Coruña, SPAIN )Lógica Modal 4 de mayo de 2006 2 / 14
Introducción
Modalidad: ¿cuál es la idea?
Capturar algún aspecto del conocimiento más frecuente en elentorno bajo estudio. Ejemplos:
instantes de tiemposiempre P(x), a_veces P(x), . . .
estados de conocimiento de un agentea_sabe_que (b_sabe_que P(x))
procesos, estados de un programa, interpretaciones de unapalabra o una frase, . . .
P. Cabalar ( Depto. Computación Universidade da Coruña, SPAIN )Lógica Modal 4 de mayo de 2006 3 / 14
Introducción
Relación con Primer Orden
¿Podríamos usar Lógica de Primer Orden?Sí, aunque con cierto “trabajo”. Ejemplo:
“siempre P(x , y)” = ∀t(Instante(t) ⇒ P(x , y , t t))
Fíjate cómo indexamos los predicados respecto a t . (reificación)
. . . de hecho, las lógicas modales son traducibles a primer orden
¿entonces para qué sirven?Notación y métodos de deducción: mucho más cómodosPerdemos expresividad, ganamos al restringir el tipo derazonamientoNormalmente, la versión proposicional es decidible
P. Cabalar ( Depto. Computación Universidade da Coruña, SPAIN )Lógica Modal 4 de mayo de 2006 4 / 14
Modal proposicional: sintaxis y axiomatización Sintaxis
Sintaxis
Cálculo Proposicional:conjunto finito de átomos o proposiciones Σ = {p, q, r , . . . }operador unario ¬operadores binarios ∧,∨,→,≡constantes >,⊥
. . . a eso añadimos 2 op. binarios:� = necesario (también representado como L)♦ = posible (también representado como M)
Prioridad de operadores: ¬, L, M,∧,∨,→,≡.
L y M son duales (podemos definir uno en func. del otro)
Mp def= ¬L¬p
P. Cabalar ( Depto. Computación Universidade da Coruña, SPAIN )Lógica Modal 4 de mayo de 2006 6 / 14
Modal proposicional: sintaxis y axiomatización Axiomatización
Axiomatización: definiciones
La sintaxis define un lenguaje L = cjto. fórmulas bien formadas
Una lógica S no es más que S ⊆ LS serán las fórmulas “válidas” o los “teoremas”
Método de deducción: axiomas + reglas de inferencia
Teorema: un axioma o una fórmula obtenida por aplicación dereglas a otros teoremas.
P. Cabalar ( Depto. Computación Universidade da Coruña, SPAIN )Lógica Modal 4 de mayo de 2006 8 / 14
Modal proposicional: sintaxis y axiomatización Axiomatización
Axiomatización: reglas de inferencia
Reglas que usaremos:
Modus Ponens (MP)` α, ` α → β
` β
Sustitución Uniforme (SU)` α
` α[β1/p1, . . . , βn/pn]
Necesitación (N)` α
` Lα
P. Cabalar ( Depto. Computación Universidade da Coruña, SPAIN )Lógica Modal 4 de mayo de 2006 9 / 14
Modal proposicional: sintaxis y axiomatización Axiomatización
Algunos axiomas básicos
Axiomas más frecuentes:
K L(p → q) → (Lp → Lq)
T Lp → p
D Lp → Mp
4 Lp → LLp
B p → LMp
P. Cabalar ( Depto. Computación Universidade da Coruña, SPAIN )Lógica Modal 4 de mayo de 2006 10 / 14
Modal proposicional: sintaxis y axiomatización Axiomatización
Ejemplo: sistema K
Es el más elemental, y está incluido en los demás.Se define a partir del axioma K
K L(p → q) → (Lp → Lq)
Ejercicio: probar los teoremas
K1 L(p ∧ q) → Lp ∧ Lq
K2 Lp ∧ Lq → L(p ∧ q)
Regla derivada:
DR1` α → β
` Lα → Lβ
P. Cabalar ( Depto. Computación Universidade da Coruña, SPAIN )Lógica Modal 4 de mayo de 2006 11 / 14
Semántica. Marcos de Kripke
Mundos posibles
En cálculo proposicional, tenemos interpretaciones
v : Σ −→ {0, 1}
que nos dan el valor de certeza de cada átomoy que ampliamos para evaluar fórmulas. Ej: v(p → ¬q)
Idea clave: manejar varios mundos, cada uno con suinterpretación proposicional.
Tendremos un mundo actual de referenciaademás de una relación que dice qué otros mundos son visiblesdesde este.
P. Cabalar ( Depto. Computación Universidade da Coruña, SPAIN )Lógica Modal 4 de mayo de 2006 12 / 14
Semántica. Marcos de Kripke
Marco Kripke (Kripke frame)
Definition (Marco Kripke)
Es un par 〈W , R〉 donde W = {w1, w2, . . . } es un conjunto de mundosy R ⊆ W ×W una relación entre mundos.
Definition (Modelo)
Es un triple 〈W , R, v〉 donde 〈W , R〉 es un marco, yv : W × Σ → {0, 1} una valoración de átomos para cada mundo.
P. Cabalar ( Depto. Computación Universidade da Coruña, SPAIN )Lógica Modal 4 de mayo de 2006 13 / 14
Semántica. Marcos de Kripke
Satisfactibilidad
Sea M = 〈W , R, v〉 un modelo. Escribimos M, w |= α para indicarque M satisface la fórmula α en el mundo w ∈ W .
P. Cabalar ( Depto. Computación Universidade da Coruña, SPAIN )Lógica Modal 4 de mayo de 2006 14 / 14