# 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 : <>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
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)`

`->`

and `*`

have the same precendece 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).
- The theorem prover has a built-in timeout, if the search for proofs for your seqeunt does not terminate in 1 minute the theorem prover just aborts the search (this shouldn't be a problem for linguistic applications)