1 Una introducción a la Lógica LinealAníbal Chehayeb Morán

2 Una introducción a la Lógica LinealContenido: Lógica Clásica vs. Lógica Lineal Conectivas de la lógica lineal Cálculo de secuentes SICStus Prolog & llprover Aplicación a las Redes de Petri

3 Una introducción a la Lógica LinealContenido: Lógica Clásica vs. Lógica Lineal Conectivas de la lógica lineal Cálculo de secuentes SICStus Prolog & llprover Aplicación a las Redes de Petri

4 Lógica Lineal vs. Lógica ClásicaEjemplo: con un euro (e) podemos comprar un paquete de Malboro (m) o un Paquete de Camel (c). En la Lógica Clásica es posible deducir a partir de las reglas anteriores: No es cierto a pesar de ser válido

5 Una introducción a la Lógica LinealContenido: Lógica Clásica vs. Lógica Lineal Conectivas de la lógica lineal Cálculo de secuentes SICStus Prolog & llprover Aplicación a las Redes de Petri

6 Conectivas de la Lógica LinealTabla de conectivas

7 Conectivas de la Lógica LinealEjemplo: Supongamos que con 5 euros nos ofrecen el siguiente menú del día en un restaurante: sopa (s) de primero, carne (c) o pescado (p) de segundo (dejándolo a nuestra elección), todo el vino (v) que queramos y, de postre flan (f) o natillas (n) dependiendo de cómo tenga el día el cocinero (esto es, la elección no depende de nosotros).

8 Conectivas de la Lógica LinealEjemplo: Supongamos que con 5 euros nos ofrecen el siguiente menú del día en un restaurante: sopa (s) de primero, carne (c) o pescado (p) de segundo (dejándolo a nuestra elección), todo el vino (v) que queramos y, de postre flan (f) o natillas (n) dependiendo de cómo tenga el día el cocinero (esto es, la elección no depende de nosotros).

9 Una introducción a la Lógica LinealContenido: Lógica Clásica vs. Lógica Lineal Conectivas de la lógica lineal Cálculo de secuentes SICStus Prolog & llprover Aplicación a las Redes de Petri

10 Cálculo de secuentes Probar que: ¿Cómo? , cálculo de secuentesDescomposición del objetivo inicial en sub-obetivos hasta llegar a situaciones en las que la solución sea trivial. Secuente:

11 Cálculo de secuentes Intuitivamente, un secuente representa el hecho de que si todas las fórmulas del antecedente son ciertas, entonces alguna del consecuente también lo es: Regla del axioma:

12 Cálculo de secuentes Resto de reglas (lógica clásica)

13 Cálculo de secuentes Por ejemplo, probar la validez de la fórmula:Árbol obtenido:

14 Una introducción a la Lógica LinealContenido: Lógica Clásica vs. Lógica Lineal Conectivas de la lógica lineal Cálculo de secuentes SICStus Prolog & llprover Aplicación a las Redes de Petri

15 SICStus Prolog Compilador comercial de Prolog (http://www.sics.se/isl/sicstus.html) Desarrollado por el Instituto Sueco de Ciencias de la Computación (SICS) Cumple el estándar ISO-Prolog Interfaz con diversos lenguajes de programación como C/C++, Java, .NET

16 SICStus Prolog

17 SICStus Prolog El predicado de unificación (=) | ?- p(A) = p(x).A = x ? yes | ?- f(X,g(b,c)) = f(Z,g(Y,c)). Y = b, Z = X ? yes

18 SICStus Prolog Ejemplo, edición del fichero ejemplo.pl% lista de hechos gusta(juan,balon). % lista de reglas futbolista(X):- gusta(X,balon). deportista(Y):- futbolista(Y).

19 SICStus Prolog Compilación, tras situarnos en el directorio correcto (File -> WorkingDirectory…): | ?- compile(ejemplo). % compiling c:/logic/ejemplo.pl.. % compiled c:/logic/ejemplo.pl in module user, 0 msec -88 bytesye Ejecución: | ?- deportista(X). X = juan ? yes

20 A Linear Logic Prover (llprover)Desarrollado por Naoyuki Tamura No comercial Válido para CLL e ILL Dos versiones: On-line: Off-line: llprover1.4.tar.gz

21 A Linear Logic Prover (llprover)llprover únicamente hace uso de caracteres convencionales (+, -, *, /, \, etc.). Es necesario establecer una correspondencia con los símbolos empleados en la LL No es necesario instalar fuentes adicionales

22 A Linear Logic Prover (llprover)Instalación y ejecución | ?- compile(llprover). % compiling c:/logic/llprover.pl... % compiled c:/logic/llprover.pl in module user, 157 msec 8 bytesyes | ?- ll. Linear Logic Prover ver 1.3 for SICStus Prolog by Naoyuki Tamura cll(full)>

23 A Linear Logic Prover (llprover)Ejemplo: cll(full)> m->(h/\r/\(c*c)),m-->h. Resultado: Ax h --> h Ax L/\1 m --> m h/\r/\c*c --> h L-> m->h/\r/\c*c,m --> h

24 Una introducción a la Lógica LinealContenido: Lógica Clásica vs. Lógica Lineal Conectivas de la lógica lineal Cálculo de secuentes SICStus Prolog & llprover Aplicación a las Redes de Petri

25 Aplicación a las Redes de PetriEjemplo

26 Aplicación a las Redes de PetriAlcanzabilidad M’=(0,0,1,1) alcanzable a partir de M=(1,0,1,2) si y sólo si el siguiente secuente es probable. Problema: el cálculo de secuentes en LL es un problema no decidible.

27 Una introducción a la Lógica Lineal¿preguntas?