An implementation of the sequent calculus to prove or disprove propositional logic formulas.

Try out an example in demo/ via npx tsx demo/tautology-2.ts. This will construct a proof tree showing that $((A \rightarrow B) \land (B \rightarrow C)) \rightarrow (A \rightarrow C)$ is a tautology. The result will look something like below. The next rule to be applied is always written at the end of the line.

Try npx tsx demo/invalid-2.ts to see how the non-tautological formula $((A \rightarrow B) \land (B \rightarrow C)) \rightarrow (C \rightarrow A)$ is disproven.