ABSTRACT. Sequent calculus is a pervasive technique for studying logics and their
properties due to the regularity of rules, proofs, and meta-property proofs
across logics. However, even simple proofs can be large, and writing them by
hand is often messy. Moreover, the combinatorial nature of the calculus makes it
easy for humans to make mistakes or miss cases. Sequoia aims to alleviate these
problems.
Sequoia is a web-based application for specifying sequent calculi and performing
basic reasoning about them. The goal is to be a user-friendly program, where
logicians can specify and "play" with their calculi. For that purpose, we
provide an intuitive interface where inference rules can be input in LaTeX and
are immediately rendered with the corresponding symbols. Users can then build
proof trees in a streamlined and minimal-effort way, in whichever calculus they
defined. In addition to that, we provide checks for some of the most important
meta-theoretical properties, such as weakening admissibility and identity
expansion, given that they proceed by the usual structural induction. In this
sense, the logician is only left with the tricky and most interesting cases of
each analysis.