Propositional sequent calculus prover
Sequent calculus is a logic system for proving/
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. |