POULE: PrOver for seqUent and Labelled systEms

General Description

POULE is a prover for linear nested sequent calculi [Lm15] for classical modal logics. It implements several systems specified in [LP15].

Syntax of Formulas

Formulas in POULE can be written as follows

    
     (Object level formulas)    F   ::=  A | F cand F | F cor F | F cimp F | box F | hearts F.
    
      
     (Labelled formulas)        L   ::=  r X F | l X F. 
   
      
     (Linear logic formulas)    M := L | M @ M | M , M | M & M | pi X\ M | sigma X\ M | top. 
   
    

References

[Lm15]	Björn Lellmann. Linear Nested Sequents, 2-Sequents and Hypersequents, accepted for publication, TABLEAUX 2015, pdf.
[LP15]	Björn Lellmann and Elaine Pimentel. Proof search in Nested Sequents, submitted to LPAR2015, pdf.

Dependencies

POULE requires the Teyjus system, an implementation of Lambda Prolog, a higher-order logic programming language.
For runnig POULE, you have to:

• Download the files llf.mod and llf.sig
• give the command tjcc llf && tjlink llf && tjsim llf
• The quest has to have the form
  llf N TH M.
  where N is the maximum depth of the proof (100 is usually enough), TH is the theory (for now either g3cp, k, kts4 or ec) and M is the linear logic clause correspondent to the object level formula to be proven. Observe that the object level formula has to be labelled with label "x".

Here there are some simple examples of queries:

System G3cp
• llf 100 g3cp (r x (a cimp a)).
• llf 100 g3cp (r x ((a cand b) cimp (a cand b))).
• llf 100 g3cp (r x ((a cand b) cimp a)).
• llf 100 g3cp (r x ((a cand b) cimp (a cor b))).
• llf 100 g3cp (r x ((a cor b) cimp (a cand b))).
• llf 100 g3cp (r x ((a cand (a cimp b)) cimp b)).

System K
• llf 100 k (r x ((box a) cimp (box a))).
• llf 100 k (r x (a cimp (box a))).
• llf 100 k (r x ((box a) cimp a)).
• llf 100 k (r x ((box (a cimp b)) cimp ((box a) cimp (box b)))).

System KTS4
• llf 100 kts4 (r x ((box a) cimp (box a))).
• llf 100 kts4 (r x ((hearts a) cimp (hearts a))).
• llf 100 kts4 (r x ((hearts a) cimp (box a))).
• llf 100 kts4 (r x ((box a) cimp (hearts a))).

And here there are some examples of theories, already included in llf's code (that is, you don't have to download them):

• Propositonal classical logic G3cp: g3cp.mod, g3cp.sig
• System K: k.mod, k.sig
• System KTS4: kts4.mod, kts4.sig
• System EC: ec.mod, ec.sig

Available soon.
We are currently working on a parser for generating automatically LL specifications out of inference figures.
This is a joint work with Carlos Olarte.

For further information, contact Björn Lellmann and Elaine Pimentel.