Prover of logic theorems in propositional calculus (using Hilbert's system of axioms). Inspired by the course of mathematical logic.
Has two modes of work:
- Prove statement: run with -p flag
- Check and annotate proof: run with -a flag
By default Prover reads statements from standard input and writes to standard output. It's possible to specify custom io files with "<" and ">" operators
- Propositional variables: (letters)(digits) : x123, y456
- Not: !x
- And: x & y
- Or: x | y
- Implies: x -> y
- Brackets: (expression)
- Header of a theorem: Assumption1, ..., AssumptionN |- Conclusion
- A -> B -> A
- (A -> B) -> (A -> B -> C) -> (A -> C)
- A -> B -> A & b
- A & B -> A
- A & B -> B
- A -> A | B
- B -> A | B
- (A -> C) -> (B -> C) -> (A | B -> C)
- (A -> B) -> (A -> !B) -> !A
- !!A -> A
Modus Ponens:
A -> B, A => B
Input:
A -> A
Output (-p flag):
|-(A->A)
((A->(A->A))->(A->(A->(A->A))))
(A->(A->A))
(A->(A->(A->A)))
(A->((A->A)->A))
((A->(A->A))->((A->((A->A)->A))->(A->A)))
((A->((A->A)->A))->(A->A))
(A->A)
If we annotate this proof with -a flag:
|-(A->A)
(1) ((A->(A->A))->(A->(A->(A->A)))) (Axiom 1)
(2) (A->(A->A)) (Axiom 1)
(3) (A->(A->(A->A))) (Modus Ponens 2 1)
(4) (A->((A->A)->A)) (Axiom 1)
(5) ((A->(A->A))->((A->((A->A)->A))->(A->A))) (Axiom 2)
(6) ((A->((A->A)->A))->(A->A)) (Modus Ponens 2 5)
(7) (A->A) (Modus Ponens 4 6)