The sequent calculus is a form of backwards reasoning, with left and right inference rules which operate on sequents. Inference rules correspond closely to clauses in the sequent, so in Logitext (and other proof-by-pointing systems), all you need to do is click on a clause to see what inference rule is triggered. In some cases, an input box will pop up; enter a lower case expression like z or f(x). (You can also choose to duplicate the rules by clicking "Contraction"). If that made no sense to you, check out the tutorial. Or, you can return to main page...