Prover for Simply Dependent Multimodal Linear Systems


Formula


T D 4

Examples

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