Propositional sequent calculus prover
Sequent calculus is a logic system for proving/deriving Boolean formulas that are true. Boolean formulas are written as sequents. A sequent S is true if and only if there exists a tree of sequents rooted at S where each leaf is an axiom and each internal node is derived from its children by an inference rule. (The full details for the rules are covered on Wikipedia and elsewhere.)
A sequent has the form (Left side formulas ⊦ Right side formulas), where the separator ⊦ in the middle is called a turnstile. The left side and right side each have zero or more Boolean formulas. The sequent (A, B, ... ⊦ X, Y, ...) is defined to mean the same as the Boolean formula (A ∧ B ∧ ...) → (X ∨ Y ∨ ...), where → is the implies operator. This is also equivalent to ¬(A ∧ B ∧ ...) ∨ (X ∨ Y ∨ ...). In plain English, the sequent means that when all the formulas on the left are true, then at least one formula on the right is true.
The JavaScript program on this page proves propositional sequents (but not predicate sequents). Namely, for a sequent S consisting of Boolean variables and Boolean operators, the program proves that for every possible truth assignment to the variables, the sequent yields the value of true. If the sequent is indeed always true, then the program outputs a proof tree of sequents. If the sequent is false in at least one truth assignment, then the proof tree will contain “Fail” somewhere within it. (The proof tree is often longer than enumerating all possible truth assignments.)
The source TypeScript code and compiled JavaScript code are available for viewing.
Program
Examples
| Summary & demo | Input | Comment |
|---|---|---|
Input syntax !&|> |
!(A & B) > !A | !B |
This represents one direction of De Morgan’s law. |
Input syntax ¬∧∨⊦ |
¬(A ∧ B) ⊦ ¬A ∨ ¬B |
This means the same as the previous example. |
| Tautology | > A | !A |
We can start with no assumptions on the left side. |
| Untrue | A | B > A & B |
This sequent is not always true. |
| Distributivity | A & (B | C) > (A & B) | (A & C) |
Distributivity of AND over OR, forward. |
| Distributivity | (A & B) | (A & C) > A & (B | C) |
Distributivity of AND over OR, backward. |
| Absorption | x | (!x & y) > x | y |
Absorption law, forward. |
| Absorption | x | y > x | (!x & y) |
Absorption law, backward. |