p q r s t 'a 'b 'c ... (propositions)
one, zero, top, bot (units)
F * G, F && G (tensor and par)
F & G, F + G (with and oplus)
!(s, F), ?(s, F) (exponentials)
s::= 1, 2, 3, ... (subexponentials)
SELL (K + 4 + T)
?(1, p) , !(1, !(1, p ^))
?(1, (p * one) + q ) , !(1, p ^)
?(1, p), ?(2, q), ?(3, r), !(1, p ^) * !(2, q ^) * !(3, r ^) * one
K
?(5, p + q) , ?(4, r + t), !(1, p ^ * t ^)
?(1, q) && ?(1, p) && !(1, p ^ * q ^)
?(1, p * q ^) && ?(1, p ^) && !(1, q)
K + 4
?(1, p), !(1, !(1, p ^))
?(3, p + q), !(2, !(1, p ^ ))
?(5, p) , ?(4, q), !(2, !(1, p ^ * q ^))
?(3, p ^) , !(2, !(1, p))
K + D
?(1,p) , ?(1, p ^)
?(2,?(1, p)) , ?(2, !(1, p ^))
?(1, ?(1, p)) && ?(1, ?(1, p ^))
K + T
?(1,p), p ^
K + D + 4
?(2, p) && ?(2, ?(1, p ^))
?(3, ?(2, p)) && ?(2, ?(1, p ^))
Description
It is well known that context dependent logical rules can be hard to both, implement and reason about. This is one of the reasons for the quest for better behaved logical systems.
Here we use linear nested sequents to propose a general framework for describing systems based on multiplicative additive linear logic plus simply dependent multimodalities. This class of systems includes linear logic with subexponentials (SELL).
This implementation is a generic way of building theorem provers for different logics, all of them based on the same grounds. The theoretical bases can be found here. For further information, please contact
Bjoern Lellmann,
Elaine Pimentel or Carlos Olarte. We thank Allan Marques
for his help in implementing this site.
The Prover
You first need to download Maude (we used the version 2.7.1).
The source files can be downloaded here.
To perform a quick test, run the Maude interpreter with the file ex_ll.maude:
maude ex_ll.maude
And then, try the following:
search [1] prove(p , p ^) =>* T .
In this case, the underlying logic is SELL (K + T + 4). Exponentials are natural numbers, all of them linear and ordered as usual.
Defining SDML
Simply dependent multimodal linear systems (SDML), different from SELL, can be defined by writing the appropriate signature (some examples are given in file signature.maude). This can be done by adapting the following template:
load ll .
fmod SIG_CONF is
protecting NAT .
protecting STRING .
protecting CONVERSION .
op U : Nat -> Bool . *** The unbounded subexponentials
op RD : Nat -> Bool . *** Subexponentials featuring D
op RT : Nat -> Bool . *** Subexponentials featuring T
op R4 : Nat -> Bool . *** Subexponentials featuring 4
op RK : Nat -> Bool . *** Subexponentials featuring K (all of them)
op _leq_ : Nat Nat -> Bool . *** The preorder relation
op toString : Nat -> String .
vars x y : Nat .
*** ======= CONFIGURABLE PART ***
eq U(x) = ToBeDefined .
eq RK(x) = ToBeDefined .
eq RT(x) = ToBeDefined .
eq R4(x) = ToBeDefined .
eq RD(x) = ToBeDefined .
eq (x leq y) = (x <= y) .
eq toString(x) = string(x, 10) .
*** ======= CONFIGURABLE PART ***
endfm
view S_CONF from SIGNATURE to SIG_CONF is
sort Subexp to Nat .
op U to U .
op RK to RK .
op RD to RD .
op RT to RT .
op R4 to R4 .
op leq to leq .
op toString to toString .
endv
mod TEST is
protecting LL{S_CONF} .
protecting TOTEX{S_CONF} .
vars T : PTree{S_CONF} .
protecting META-LEVEL * (
op _,_ : Set{X} Set{X} -> Set{X} to comma ,
op _,_ : Map{X,Y} Map{X,Y} -> Map{X,Y} to comma ,
op _,_ : NeGroundTermList GroundTermList -> NeGroundTermList to comma ,
op _+_ : ModuleExpression ModuleExpression -> ModuleExpression to plus
) .
endm
Change the "ToBeDefined" parts with true/false as needed. It is also possible to use a different signature for the subexponentials. See for instance the signature SIG_TIME in signature.maude.