Glue Logic theorem prover

Sequents syntax

Sequents should be read as stating that the resources on the left of => when combined generate single resource on the right (the calculus is linear and intuitionistic).

There are three connectives: -> which is linear implication, *, multiplicative "and", and <> which represents the monadic "modality".

The calculus is "typed", but you have to specify types only for atoms. The types are mainly necessary because we have variables.

You can specify for each lexical resource a constant that represents its lexical meaning, or let the program supply a rather uninformative variable

Examples:

everyone : (e.e -> X.t) -> X.t, love : e.e -> s.e -> l.t, someone : (s.e -> Y.t) -> Y.t => l.t

reza : r.e, not : b.t -> b.t, believe : <>i.t -> r.e -> <>b.t, jesus : <>j1.e, is : j1.e -> j2.e -> i.t, jesus : <>j2.e => <>b.t

a.a * b.b, a.a -> b.b -> c.c => c.c

a.a -> b.b, a.a => b.b

(these last two examples are just to show that you can also avoid specifying the meaning terms, the theorem prover will generate generic variables for you)

BNF grammar:

Literals are indicated by double quotes. White spaces are irrelevant, put as many as you like.

Sequent := LHS "=>" RHS
LHS := "" | Formula "," LHS
RHS := SimpleFormula
Formula := DecoratedFormula | SimpleFormula
DecoratedFormula := Constant ":" SimpleFormula
Constant := [a-ZA-Z0-9]+
SimpleFormula := ["("] (Atom | Variable | Implication | Tensor | Monad) [")"]
Atom := [a-z][a-zA-Z0-9]* "." Type
Type := [a-zA-Z0-9]+
Variable := [A-Z][a-zA-Z0-9]* "." Type
Implication := SimpleFormula "->" SimpleFormula
Tensor := SimpleFormula "*" SimpleFormula
Monad := "<>" SimpleFormula

Notes:

Parentheses are always optional
Types are only specified on atoms and variables, the type of complex formulae is inferred
<> binds tighter than -> and *, so <>a.a -> b.b is equivalent to (<>a.a) -> b.b
-> is right associative, so a.a -> b.b -> c.c is equivalent to a.a -> (b.b -> c.c)
Similarly * is right associative, so a.a * b.b * c.c is equivalent to a.a * (b.b * c.c)
* has higher precedence than -> so a.a * b.b -> c.c is equivalent to a.a * (b.b -> c.c)
Variables used in different formulae should be given different names (unless you want to create a dependency between the instantiation of a variable in one formula with the one in another).