Ejercicios con LWB para el Seminario Monográfico de Lógica:
Introducción a las lógicas no-monotónicas

Primavera de 2004 (Semestre 2004-2)
Dr. Raymundo Morado

• Ejercicio 1:  Familiarícese con LWB,  Logics Workbench. Desarrollada en la Universidad de Berna en Suiza, permite trabajar con lógicas proposicionales como la clásica, la intuicionista, las modales K, KT, S4, S5, y G, las multimodales Kn, KTn, y S4n, las temporales PLTL y TK, la lineal. Especialmente nos interesan las lógicas proposicionales no monotónicas: autoepistémica, default, de circunscripción y de mundo cerrado.

• Ejercicio 2: Use LWB para generar las teorías bajo el supuesto de mundo cerrado (CWA) en los siguientes ejemplos:

(1a)
load(cwa);
cwa([p0 & p1, p0 v p2]);
(1b)
load(cwa);
set("infolevel", 7);
cwa([p0 & p1, p0 v p2]);
(2)
load(cwa);
set("infolevel", 8);
cwa([p0 -> p1, p1, p2 & p3]);
(3)
load(cwa);
set("infolevel", 6);
consistent([p0 v p1]);
(4)
load(cwa);
set("infolevel", 4);
cwa([p0 v p1], [p0]);
(5)
load(cwa);
set("infolevel", 4);
consistent([p0 v p1], [p0]);
(6)
load(cwa);
set("infolevel", 4);
cwa([p0 v p1], [p1,p2,p3]);
(7)
load(cwa);
set("infolevel", 3);
cwa([p0 v p1 v p2], [p1, p2, p3]);
(8)
load(cwa);
set("infolevel", 3);
consistent([p0, p1 v p2]);
(9)
load(cwa);
set("infolevel", 8);
consistent([p0, p1 v p2], [p0, p1]);
(10)
load(cwa);
set("infolevel", 8);
provable(p1 & ~p2, [p0, p0 -> p1]);
(11)
load(cwa);
set("infolevel", 8);
provable(~p3 & ~p4, [p0, p1], [p1, p3]);
(12)
load(cwa);
set("infolevel", 8);
provable(~p3 & ~p4, [p0, p1], [p1, p3, p4]);

• Ejercicio 3: Use LWB para generar las extensiones de los siguientes seis ejemplos tomados de Reiter (A Logic for Default Reasoning):

2.1, p. 72
load(default);
extensions([ [B -> ~A & ~C], [ [true, A, A],
                               [true, B, B],
                               [true, C, C] ] ]);
2.2, p. 72
load(default);
extensions([ [true], [ [true, C, ~D],
                       [true, D, ~E],
                       [true, E, ~F] ] ]);
2.3, p. 72
load(default);
extensions([ [true], [ [true, C, ~D],
                       [true, D, ~C] ] ]);
2.4, p. 73
load(default);
extensions([ [B,
              C -> D v A,
              A & C -> ~E], [[ true,           A, A],
                             [    B,           C, C],
                             [D v A,           E, E],
                             [C & E, [~A, D v A], F]] ]);
2.5, p. 73
load(default);
extensions([ [true], [ [   A,  E,  E],
                       [true,  A,  A],
                       [true, ~A, ~A] ] ]);
2.6, p. 73
load(default);
extensions([ [true], [ [true, A, ~A] ] ]);

• Ejercicio 3: Proponga una teoría default, formalícela, y genere sus extensiones con LWB.