• Ejercicio 1:  Familiarícese con LWB.  [The Logics Workbench (LWB) is developed at the University of Bern in Switzerland.  The LWB offers the possibility to work in a user-friendly way in classical and non-classical propositional logics, including nonmonotonic approaches.  It supports the classical and intuitionistic propositional logic, the modal propositional logics K, KT, S4, S5, and G, the multimodal propositional logics Kn, KTn, and S4n, the temporal propositional logic PLTL and the tense propositional logic TK, the linear propositional logic, and the nonmonotonic propositional autoepistemic logic, default logic, circumscription and default logic. For these logics, the LWB offers functions concerning provability, formula simplification, computation of normal forms, and embeddings, among others.]

• Ejercicio 2: 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.