A brief explanation of the output

Each line of a proof consists of a list of RL terms, the sequent turnstile !-, another RL term, and finally the name of a rule that was applied to derive this line. There are left and right rules for each of the operation symbols in the language of residuated lattices. Gentzen system rules are usually written in a positive style, with a list of premises above a horizontal line, followed by the conclusion below. When searching for a proof, such rules are applied from bottom to top, producing trees that grow upwards, and expand in width very rapidly. Such proofs are not easily displayed on a webpage, so here we use a different approach based on the Fitch style of presenting natural deduction proofs.

(Reformated rules to be inserted here...)

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.