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. 


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


POULE requires the Teyjus system, an implementation of Lambda Prolog, a higher-order logic programming language.
For runnig POULE, you have to:
Here there are some simple examples of queries: And here there are some examples of theories, already included in llf's code (that is, you don't have to download them):
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.