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
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)
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
<>binds tighter than
<>a.a -> b.bis equivalent to
(<>a.a) -> b.b
->is right associative, so
a.a -> b.b -> c.cis equivalent to
a.a -> (b.b -> c.c)
*is right associative, so
a.a * b.b * c.cis equivalent to
a.a * (b.b * c.c)
*have the same precendece so
a.a * b.b -> c.cis equivalent to
a.a * (b.b -> c.c)