okay-prove

Propositional logic proof generator written in TypeScript

Usage

You can interact with it using one of these front-end interfaces:

• Command-Line Interface - okay-prove-cli

Or as a library in your own code:

• okay-prove on npm

High-Level Prompt Format

a
b
a and b

The last line is the conclusion. Every other line is a premise.

Symbols

Symbols can be any combination of the characters A-Z, a-z, 0-9 and _.

Operators

Operators include and, or, not and implies, with not having the highest precedence and implies having a lower precedence than and and or.

Groups

Expressions can be grouped together by parentheses - e.g. (a implies b) and (b and c)

Tautologies

Tautologies are written with a period - e.g. .

Contradictions

Contradictions are written with an exclamation point - e.g. !

Example Proofs

Example #1

Prompt (in high-level input format):

(q and (a or b)) or ((b or a) and r)
b or a

Proof (visualized in "inline" format):

 1. (q and (a or b)) or ((b or a) and r) [premise]
 2. (q and (a or b)) or ((a or b) and r) [commutative : 1]
 3. ((a or b) and q) or ((a or b) and r) [commutative : 2]
 4. (a or b) and (q or r)                [distributive : 3]
 5. a or b                               [specialization : 4]
 6. b or a                               [commutative : 5] ☐

Example #2

Prompt (in high-level input format):

p or not (r or q)
s implies r
not p
not s

Proof (visualized in "inline" format):

 1. not p             [premise]
 2. p or not (r or q) [premise]
 3. not (r or q)      [elimination : 2, 1]
 4. not r and not q   [de morgan's : 3]
 5. not r             [specialization : 4]
 6. s implies r       [premise]
 7. not s             [modus tollens : 6, 5] ☐

Example #3

Prompt (in high-level input format):

p implies (q implies r)
not ((q implies r) and s)
not (p and s) implies u and w
x implies not u
s
not x

Proof (visualized in "inline" format):

 1. s                               [premise]
 2. not ((q implies r) and s)       [premise]
 3. not ((not q or r) and s)        [definition of implies : 2]
 4. not (not q or r) or not s       [de morgan's : 3]
 5. not (not q or r)                [elimination : 4, 1]
 6. p implies (q implies r)         [premise]
 7. p implies (not q or r)          [definition of implies : 6]
 8. not p                           [modus tollens : 7, 5]
 9. not p or not s                  [generalization : 8]
10. not (p and s)                   [de morgan's : 9]
11. not (p and s) implies (u and w) [premise]
12. u and w                         [modus ponens : 11, 10]
13. u                               [specialization : 12]
14. x implies not u                 [premise]
15. not x                           [modus tollens : 14, 13] ☐