Download Método de los Árboles Semánticos

Sistemas Lgicos Computacionales
Curso académico 2007/2008
Tema 3: Método de los Árboles Semánticos
Guido Sciavicco
Universidad Murcia, Espinardo (Murcia) - Spain
– p. 1/?
La Maquina que Piensa
Formalizar el razonamiento (el pensamiento) tiene un
objetivo especifico, de carácter puramente practico, que
va más allá del puro conocimiento;
Si un “sistema” de razonamiento es suficientemente
formal como para ser reducido a un conjunto de pasos,
entonces puede ser transformado en un programa para
ordenador (o sea es un algoritmo);
Deber del diseñador de un tal algoritmo es demostrar
que se trata de un algoritmo correcto, en un sentido
que aclaramos a continuación.
– p. 2/?
La Maquina que Piensa (cont.)
Cualquier ordenador pasado, presente, y futuro (en
ciertos sentidos) debe contar con dos limitaciones
físicas: el tiempo de computación y el espacio de
memoria son finitos;
Por lo tanto, cualquier algoritmo debe terminar en un
tiempo finito y (por lo menos parcialmente) predecible,
y utilizar una cantidad de espacio finito y (por lo menos
parcialmente) predecible;
Un algoritmo con éstas características se denomina
terminante;
– p. 3/?
La Maquina que Piensa (cont.)
Además, querremos que nuestro algoritmo, siempre
que nos de una respuesta, ésta respuesta sea correcta,
y denominaremos un tal algoritmo correcto;
Finalmente, querremos que nuestro algoritmo no se
“olvide” ninguna posible respuesta correcta, y
denominaremos un tal algoritmo completo;
En términos de lógica, un algoritmo deductivo es un
algoritmo capaz, dada una formula en su lenguaje,
decir si la formula es o menos satisfactible (o es una
tautologia, o es una contradicción), utilizando, por cada
φ, los resultados que ya conocemos:
φ tautologia ⇔ ¬φ contradiccion
y. . .
– p. 4/?
La Maquina que Piensa (cont.)
...
φ satisf actible ∧ ¬φ satisf actible ⇔ φ contingencia
o sea no es ni una tautología ni una contradicción;
Pero, es esto posible para cualquier lógica?
La respuesta es NO. Para lo que nos concierne, es
posible para la Lógica Proposicional, pero no para la
Lógica de Primer Orden;
En concreto, para éste ultimo caso, todos los algoritmo
correctos y completos fallan en la terminación, es decir,
el poder expresivo es tan alto que cualquier algoritmo
correcto y completo puede necesitar de un tiempo
infinito de computación.
– p. 5/?
La Maquina que Piensa (cont.)
Un conjunto de símbolos, con una gramática para la
generación de las formulas y una semántica bien
definida, o sea, una lógica, se denomina decidible si
posee por lo menos un algoritmo de deducción
correcto, completo y terminante, y no decidible en caso
contrario;
Ésta definición, en términos más generales, se aplica a
cualquier clase de problemas, y la hemos tomada en
préstamo desde la teoría de la computabilidad, que
tiene sus raíces en Gödel, Turing, Church, a partir de
los años 40.
– p. 6/?
Razonando con Proposiciones
A nivel de la Lógica Proposicional, formalizar un
sistema automático de deducción resulta bastante
sencillo;
Por el momento, nos centraremos en un sistema
basado en la semántica de las formulas, que por lo
tanto se llama sistema de los árboles semánticos o
tableaux (es decir, tablas);
Las reglas de éste sistema se basan una a una en las
reglas semánticas que ya hemos visto;
Por ejemplo, deduciremos p a partir de ¬¬p, o
deduciremos q a partir de p → q y p.
– p. 7/?
Vamos con Juicio
Un juicio es un afirmación del tipo V.φ o F.φ, donde φ es
una fórmula;
En términos prácticos, nosotros nos preguntaremos,
dada una fórmula, si V.φ vale, o sea, si φ es una
tautología, o, si es conveniente, si F.φ vale, o sea, si φ
es una contradicción;
La cosa más sencilla para demostrar si es un caso o el
otro es encontrar un contra-modelo, o sea una
interpretación tal que la formula NO se satisface;
Por ejemplo, si quiero demostrar que F.φ (φ es una
contradicción), donde φ = p ∧ ¬p, es suficiente enseñar
la interpretación I = {p = V }, porque evidentemente
I 6|= p ∧ ¬p.
– p. 8/?
Reglas
Vamos a ver las reglas formales:
1. V.¬φ ⇒
V.¬φ
F.φ
V.φ ∧ ψ
2. V.φ ∧ ψ ⇒
V.φ
V.ψ
F.φ ∨ ψ
3. F.φ ∨ ψ ⇒
F.φ
F.ψ
F.¬φ ⇒
F.¬φ
V.φ
F.φ ∧ ψ
F.φ ∧ ψ ⇒
F.φ
F.ψ
V.φ ∨ ψ
V.φ ∨ ψ ⇒
V.φ
V.ψ
– p. 9/?
Reglas (cont.)
F.φ → ψ
4. F.φ → ψ ⇒
V.φ
F.ψ
V.φ → ψ
V.φ → ψ⇒
F.φ
V.ψ
– p. 10/?
El Algoritmo
Se empieza con una formula proposicional φ;
Si quiero demostrar que φ ES una tautología, intentaré
demostrar que F.φ NO es satisfacible;
Aplico las reglas a F.φ, teniendo en cuenta:
1. Se aplica la regla al juicio “más arriba” que todavia
no ha sido considerado;
2. Se aplica la regla a TODAS las ramas ACTIVAS
(véase punto siguiente);
3. Si una rama contiene el juicio V.p Y el juicio F.p,
entonces es una rama contradictoria y es preciso
cerrarla (NO ACTIVA).
– p. 11/?
Un Ejemplo Sencillo
Queremos demostrar que la formula (p ∧ (p → q)) → q
es una tautología; verifiquemos F.φ:
√
F.(p ∧ (p → q)) → q
√
V.(p ∧ (p → q))
F.q
V.p
V.(p → q)
F.p
√
V.q
– p. 12/?
Conclur desde un Árbol Semántico
Al final del desarollo del árbol, cada rama ACTIVA es
un modelo para el juicio;
Si el juicio de salida era V.φ, entonces una rama
ACTIVA es un modelo para la formula φ, mientras si era
F.φ es un modelo para la formula ¬φ;
Si no hay ramas ACTIVAS, el juicio de salida es
insatisfactible; por ejemplo, si se trataba de un juicio del
tipo V.φ, entonces φ es insatisfactible, o sea ¬φ es una
tautología.
– p. 13/?
Entonces:
Si quiero demostrar que φ es satisfactible ⇒ expando
V.φ, y cada rama ACTIVA al final del proceso
representa un modelo para φ;
Si quiero demostrar que φ es una tautología, expando
F.φ y verifico que no hay ninguna rama ACTIVA al final
del proceso;
Si quiero demostrar que φ es una contradicción,
expando V.φ, y verifico que al final del proceso no hay
ninguna rama ACTIVA;
Como es la formula del ejemplo anterior?
– p. 14/?
Ejercicios
Elegir una regla de trasformación cualquiera y
demostrar que se trata de una tautología con el método
de los árboles semánticos;
Demostrar que las siguientes son formulas
satisfactibles:
φ1 = p ∧ (p → (q ∨ r)) ∧ ¬r;
φ2 = (p ∨ q) ∧ ¬p ∧ (q → r) ∧ ¬¬r;
Demostrar que las siguientes son tautologías:
φ3 = (¬p ∧ (q → p)) → ¬q ;
φ4 = ((p → q) ∧ (q → r)) → (p → r).
– p. 15/?
Extender el Algoritmo al Primer Orden
Al Primer Orden la cosa se complica un poco: debemos
tener en cuenta:
Variables, constantes, símbolos funcionales y
términos;
Cuantificadores;
Debemos tener presente que al Primer Orden NO
EXISTE una técnica deductiva terminante, por lo tanto
nuestro algoritmo puede ser correcto, completo pero no
necesariamente terminará siempre su computación!
– p. 16/?
Qué Podemos Computar?
La razón intuitiva de los “problemas” que tenemos al
Primer Orden, es que para demostrar que ciertas
fórmulas son satisfactibles, debemos mostrar un
modelo infinito. . .
. . . y el espacio y el tiempo que tenemos a disposición
son finitos;
Pero, al Primer Orden es siempre posible demostrar
que una formula NO es satisfactible en tiempo y
espacio finitos!
Por lo tanto, siempre que una formula sea una
tautología, podremos demostrarlo (recuerda: φ
tautología ⇔ ¬φ no satisfactible);
Para mantener las cosas simples, nos centraremos
solo en formulas cerradas.
– p. 17/?
Razonemos
Como podemos demostrar que una formula de Primer
Orden es insatisfactible?
La parte proposicional de la formula se trata como
hemos visto anteriormente;
Constantes, variables y símbolos funcionales debes ser
tratados de forma “abstracta”; por ejemplo, para
demostrar que la formula
∀xP (x) ∧ ¬P (a)
no es satisfactible, NO ES SUFICIENTE interpretar,
digamos, x y a como numeros naturales (recuerda: no
satisfactible = no existe NINGUNA interpretación,
dominio, . . . ).
– p. 18/?
Interpretaciones Abstractas
Sabemos que la insatisfactibilidad de una formula
depende solamente de su estructura lógica;
Utilizaremos por lo tanto interpretaciones abstractas,
llamadas de Herbrand (por su inventor) que nos
permitiran evitar cualquier hipótesis sobre el dominio y
sus propiedades;
Éstas interpretaciónes dependen exclusivamente del
lenguaje que se utiliza en la formula en cuestión.
– p. 19/?
Interpretaciones Abstractas (cont.)
En general, el dominio es el conjunto de las constantes
de la formula (o conjunto con una sola constante si la
formula no contiene ninguna) + conjunto de todas las
aplicaciones posibles de símbolos funcionales del
lenguaje (si hay) a elementos del dominio;
Ejemplo: el dominio de una interpretación de Herbrand
para la formula φ = ∀x(P (x) ∧ Q(f (x))) ∨ R(a, b) es
DH = {a, b, f (a), f (b), f (f (a)), f (f (b)), . . .}
Ahora, simplemente mirando el numero de parámetros
de cada símbolo de predicado, obtenemos una
interpretación; por ejemplo, en el caso anterior. . .
– p. 20/?
Interpretaciones Abstractas (cont.)
. . . podríamos tener:
1 = (D , P = ∅, Q = ∅, R = ∅);
IH
H
H
H
H
2 = (D , P = {a}, Q = ∅, R = ∅);
IH
H
H
H
H
3 = (D , P = ∅, Q = {a}, R = ∅);
IH
H
H
H
H
4 = (D , P = {a}, Q = ∅, R = {(a, b), (a, f (a))});
IH
H
H
H
H
...
. . . y muchas otras (son infinitas, en éste caso!);
Como cualquier interpretación, una IH puede o no
satisfacer la formula; en éste caso tenemos, por
4 |= φ.
ejemplo, que IH
– p. 21/?
Tomando Confianza con Herbrand
Se consideren las siguientes formulas:
∀x, y(P (x, y) → Q(x) ∨ R(y));
∀x(P (x) → Q(x)) ∧ P (a) ∧ ¬Q(a);
∀x(P (x) → Q(f (x))) ∧ P (a) ∧ ¬Q(b).
Y por cada una de ellas, se encuentre, si es posible,
una interpretación de Herbrand que la satisface y una
que no la satisface.
– p. 22/?
Para Qué?
Las interpretaciones de Herbrand tienen una
característica muy importante que nos ayudará a
desarrollar una metodología de deducción;
Hemos visto que una tal interpretación tiene un dominio
bien definido, que se denomina base de Herbrand;
Cualquier interpretación de Herbrand que utilize como
dominio la base de Herbrand (de su lenguaje) más un
conjunto cualquiera de (nuevas) constantes se
denomina interpretación extendida de Herbrand;
Teorema: cualquier formula de Primer Orden cerrada
es satisfactible si y solo si lo es en una interpretación
extendida de Herbrand.
– p. 23/?
Reglas
El papel jugado en el caso de la logica Proposicional
por las letras proposicionales, ahora lo juegan las
formulas atómicas;
Por lo tanto, no habrá regla para los juicios
V.p(t1 , . . . , tn ) y F.p(t1 , . . . , tn );
Gracias al teorema que hemos visto, podemos buscar
solo en el mundo de las interpretaciones que tienen
como dominio la base (extendida) de Herbrand;
Si la formula en cuestión no contiene constantes,
entonces se empieza con DH = {a}, donde a no
aparece en el lenguaje, mientras si contiene por lo
menos una constante, DH será la base de Herbrand.
– p. 24/?
Reglas (cont.)
Nuevas reglas formales:
5. V.∀xφ(x)
⇒
V.∀xφ(x)
V.φ(t)
F.∀xφ(x)
F.∀xφ(x)⇒
F.φ(s)
V.∀xφ(x)
6. F.∃xφ(x)
⇒
V.∃xφ(x)
F.∃xφ(x)
F.φ(t)
V.∃xφ(x)⇒
V.φ(s)
F.∃xφ(x)
– p. 25/?
Reglas (cont.)
t es el primer término de la base de Herbrand DH que
no aún no ha sido utilizado para la sustitución en la
formula ∀xφ(x), y
s es el primer término de la base de Herbrand DH que
no aún no ha sido utilizado en la rama, o una nueva
constante, que se añade a la base actual, si no hay
ningún término disponible.
– p. 26/?
Ejemplo
φ = (∀x(p(x) → p(f (x))) ∧ p(a)) → p(f (a)) es una
tautología:
√
F.(∀x(p(x) → p(f (x))) ∧ p(a)) → p(f (a))
DH = {a, f (a), . . .
V.∀x(p(x) → p(f (x)))
√
V.p(a)
F.p(f (a))
V.(p(a) → p(f (a)))
√
V.∀x(p(x) → p(f (x)))
F.p(a)
V.p(f (a))
– p. 27/?
. . . Y más Ejercicios
Elegir una regla de trasformación relativa a los
cuantificadores y demostrar que se trata de una
tautología con el método de los árboles semánticos;
Demostrar que las siguientes son tautologías:
φ1 = (∀x, y(P (x, y) → ∃zR(z)) ∧ ∀x¬R(x)) → ¬P (a, b);
φ2 = (P (a) ∨ P (f (a))) → ¬∀x¬P (x);
φ3 = (∀x∃y(P (x) → ¬R(y))) → ¬∃x∀y(P (x) ∧ R(y)).
– p. 28/?