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)
  

?(1, p) , !(1, !(1, p ^))
?(1, (p * one) + q ) , !(1, p ^)
?(1, p), ?(2, q), ?(3, r), !(1, p ^) * !(2, q ^) * !(3, r ^) * one
  

?(5, p + q) , ?(4, r + t), !(1, p ^ * t ^) 
?(1, q)  && ?(1, p)  && !(1, p ^ * q ^)
?(1, p * q ^) && ?(1, p ^) && !(1, q)
  

?(1, p), !(1, !(1, p ^))
?(3, p + q), !(2, !(1, p ^ ))
?(5, p) , ?(4, q), !(2, !(1, p ^ * q ^))
?(3, p ^) , !(2, !(1, p))
  

?(1,p) , ?(1, p ^)
?(2,?(1, p)) , ?(2, !(1, p ^))
?(1, ?(1, p)) && ?(1, ?(1, p ^))
  

?(1,p), p ^
  

?(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.