JUMP TO

mllprover: a prover for modal Linear Logic

individual biat prover: a prover for the modal Linear Logic of individual agency

coalitional biat prover: a prover for the modal Linear Logic of coalitional agency


mllprover: a prover for modal Linear Logic

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)> 


individual biat prover: a prover for the modal Linear Logic of agency

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 as
When 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)]])).