mllprover is a simple extension of Naoyuki Tamura's Linear Logic Prover with a non-normal modality #. The theoretical background is presented in Daniele Porello, Nicolas Troquard: Non-normal modalities in variants of Linear Logic. CoRR abs/1503.04193 (2015) The source code can be found here.
This is more a proof of concept than a practical implementation of reasoning.
The code comes with a few implemented rules: re(#) (rule of equivalents), refl(#) (reflexivity rule, axiom T), trans(#) (transitivity rule, axiom 4, ...), c(#) (contraction). trans(#) and c(#) are commented out in the linked sources.
The code comes with a few suggested examples, too.
Note that mllprover is not restricted to a particular fragment of Linear Logic. It works with intuitionistic propositional Linear Logic as well as with full Linear Logic with exponentials.
We use SWI-Prolog in the following example.
user@computer:~$ swipl
% library(swi_hooks) compiled into pce_swi_hooks 0.00 sec, 3,856 bytes
Welcome to SWI-Prolog (Multi-threaded, 64 bits, Version 5.10.4)
Copyright (c) 1990-2011 University of Amsterdam, VU Amsterdam
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software,
and you are welcome to redistribute it under certain conditions.
Please visit http://www.swi-prolog.org for details.
For help, use ?- help(Topic). or ?- apropos(Word).
?- ['mllprover.pl'].
% mllprover.pl compiled 0.01 sec, 184,232 bytes
true.
?- ll.
Linear Logic Prover ver 1.3 for SICStus Prolog
http://bach.seg.kobe-u.ac.jp/llprover/
by Naoyuki Tamura (tamura@kobe-u.ac.jp)
cll(full)> [s, s*f->t, #f] --> t.
[s,s*f->t,#f]-->t.
Trying to prove with threshold = 0
Succeed in proving s,s*f->t,#f --> t (0 msec.)
twosided:pretty:1 =
------- Ax
f --> f
------- Ax -------- refl(#)
s --> s #f --> f
-------------------- R* ------- Ax
s,#f --> s*f t --> t
---------------------------- L->
s,s*f->t,#f --> t
yes
cll(full)> # (!a*!b)--> #! (a/\b).
# (!a*!b)--> #! (a/\b).
Trying to prove with threshold = 0 1
Succeed in proving # (!a*!b) --> #! (a/\b) (10 msec.)
twosided:pretty:2 =
------- Ax ------- Ax ------- Ax ------- Ax
a --> a b --> b a --> a b --> b
-------- L! -------- L! ---------- L/\1 ---------- L/\2
!a --> a !b --> b a/\b --> a a/\b --> b
----------- W! ----------- W! -------------- L! -------------- L!
!a,!b --> a !a,!b --> b ! (a/\b) --> a ! (a/\b) --> b
--------------------------- R/\ --------------- R! --------------- R!
!a,!b --> a/\b ! (a/\b) --> !a ! (a/\b) --> !b
------------------ R! ----------------------------------- R*
!a,!b --> ! (a/\b) ! (a/\b),! (a/\b) --> !a*!b
------------------ L* --------------------------- C!
!a*!b --> ! (a/\b) ! (a/\b) --> !a*!b
----------------------------------------------------- re(#)
# (!a*!b) --> #! (a/\b)
yes
cll(full)>
An instantiation for the logic of agency of bringing-it-about can be found here. It supports a slightly different language. biat(a1,p) is a formula representing the agent a1 bringing about p. The formula biat(a3,p*q) represents the agent a3 bringing about p*q. The set of agents is {a1,a2,a3,a4,a5,a6,a7,a8,a9}. See the source code for details and suggested examples.
Fundamental rules of agency have been implemented. (See details in Daniele Porello, and Nicolas Troquard. A resource-sensitive logic of agency. In 21st European Conference on Artificial Intelligence (ECAI'14), Prague, Czech Republic. IOS Press, 2014, pages 723-728.) They are:
% rule of equivalents A --> B B --> A ---------------------------------- (re(ai)) biat(ai,A) --> biat(ai, B) % reflexivity rule, axiom T X, biat(ai,A) --> B ------------------- (refl(ai)) X, A --> B % rule of non-trivial agency --> B ------------------ (necneg(ai)) biat(ai,B) --> bot % rule combine-with X --> biat(ai,A) X --> biat(ai,B) ---------------------------------- (wcomb(ai)) X --> biat(ai, A /\ B) % rule combine-tensor % Careful. this is a dubious rule of agency! X1 --> biat(ai,A) X2 --> biat(ai,B) ------------------------------------ (tcomb(ai)) X1,X2 --> biat(ai, A * B)We present two proofs in Linear BIAT with the following example.
user@computer:~$ swipl % library(swi_hooks) compiled into pce_swi_hooks 0.00 sec, 3,856 bytes Welcome to SWI-Prolog (Multi-threaded, 64 bits, Version 5.10.4) Copyright (c) 1990-2011 University of Amsterdam, VU Amsterdam SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software, and you are welcome to redistribute it under certain conditions. Please visit http://www.swi-prolog.org for details. For help, use ?- help(Topic). or ?- apropos(Word). ?- ['individual_biat_prover.pl']. % individual_biat_prover.pl compiled 0.01 sec, 191,336 bytes true. ?- ll. Linear Logic Prover ver 1.3 for SICStus Prolog http://bach.seg.kobe-u.ac.jp/llprover/ by Naoyuki Tamura (tamura@kobe-u.ac.jp) cll(full)> biat(a1,s*f->t),biat(a2,p->f),biat(a3,p),s-->t. biat(a1,s*f->t),biat(a2,p->f),biat(a3,p),s-->t. Trying to prove with threshold = 0 Succeed in proving biat(a1,s*f->t),biat(a2,p->f),biat(a3,p),s --> t (30 msec.) twosided:pretty:1 = ------- Ax p --> p ---------------- refl(a3) ------- Ax biat(a3,p) --> p f --> f ---------------------------------- L-> p->f,biat(a3,p) --> f ------- Ax ------------------------------ refl(a2) s --> s biat(a2,p->f),biat(a3,p) --> f ------------------------------------------ R* ------- Ax biat(a2,p->f),biat(a3,p),s --> s*f t --> t -------------------------------------------------- L-> s*f->t,biat(a2,p->f),biat(a3,p),s --> t ------------------------------------------------ refl(a1) biat(a1,s*f->t),biat(a2,p->f),biat(a3,p),s --> t yes cll(full)> biat(a5,r1), biat(a5,r2), biat(a9, (biat(a5,r1/\r2)-> m)) --> m. biat(a5,r1),biat(a5,r2),biat(a9,biat(a5,r1/\r2)->m)-->m. Trying to prove with threshold = 0 Succeed in proving biat(a5,r1),biat(a5,r2),biat(a9,biat(a5,r1/\r2)->m) --> m (10 msec.) twosided:pretty:2 = --------------------------- Ax --------------------------- Ax biat(a5,r1) --> biat(a5,r1) biat(a5,r2) --> biat(a5,r2) ----------------------------------------------------------- wcomb(a5) ------- Ax biat(a5,r1),biat(a5,r2) --> biat(a5,r1/\r2) m --> m ---------------------------------------------------------------------- L-> biat(a5,r1),biat(a5,r2),biat(a5,r1/\r2)->m --> m --------------------------------------------------------- refl(a9) biat(a5,r1),biat(a5,r2),biat(a9,biat(a5,r1/\r2)->m) --> m yes cll(full)>
WORK IN PROGRESS: AGENCY OF COALITIONS
Coalitions can be any list containing agents: here. We find some rules that allow to aggregate the agency of coalitions. For instance we find such rules asWhen C1 and C2 are independent/do not share any agent: X1 --> modal([a1,a3],A) X2 --> modal([a4,a2,a7],B) --------------------------------------------------- X1,X2 --> modal([a1,a2,a3,a4,a7], A * B) % rule combine-tensor (optionally with superadditivity) rule([ill,0], no, comb(mod), S, [S1, S2], [[l(0),r(0)],[l(0),r(0)],[l(0),r(0)]]) :- match(S, ([X]-->[[modal(C,A*B)]])), merge(X1,X2,X), coalitionmerge(C1,C2,C), coalitionq(C1), coalitionq(C2), coalitionindep(C1,C2), % superadditive version % comment out otherwise match(S1, ([X1]-->[[modal(C1,A)]])), match(S2, ([X2]-->[[modal(C2,B)]])).