# Glue Logic theorem prover

Sequent to prove:

## 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 : <>r.e -> <>i.t -> <>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 variable 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
• `<>` 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)`
• `->` and `*` have the same precendece so `a.a * b.b -> c.c` is equivalent to `a.a * (b.b -> c.c)`