The (in)equations are in the language of (bounded) residuated lattices. Specifically, the language used here has
A list of standard equational results about residuated lattices can be viewed on this page.
Test yourself by deciding the following randomly generated RL equations.
To display the proofs in a linear fashion, rather than the more usual Gentzen style, the proof trees are displayed from the root downwards, with the depth of nodes indicated by the indentation level. (Only the branching rules increase the indentation depth.) Each sequent is labeled by the name of the rule that produced it. When a terminal node is reached, the indentation level decreases again. With a bit of practice, these proofs are actually easier to read (and write) than the standard tree-like presentation. The symbol !- can be interpreted as not less or equal, in which case each line implies the one below it (if at the same indentation level) or one of the two indented alternatives (in the case of a branching rule). With this interpretation, the terminal nodes represent contradictions, reminiscent of a tableau style proof.