## POULE: PrOver for seqUent and Labelled systEms |

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

[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. |

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

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.

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.