theorem-prover 0.1.1

Implementation of a theorem prover for first-order logic.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12

p(x) \/ ~p(x)
(forall x.(p(x))) -> p(x)
(forall x.(p(x))) -> (exists x.(p(x)))
(forall x.(p(x))) -> (forall y.(p(y)))
(forall x.(p(x) \/ q(x))) -> (exists x.(p(x)) \/ forall x.(q(x)))
(forall x.(p(x) /\ q(x))) -> (forall x.(p(x)) /\ forall x.(q(x)))
(forall x.(p(x) -> q(x))) -> (forall x.(p(x)) -> forall x.(q(x)))
(exists x.(p(x) /\ q(x))) -> (exists x.(p(x)) /\ exists x.(q(x)))
(exists x.(p(x)) /\ forall x.(p(x) -> q(x))) -> exists x.(q(x))
~(exists y.(forall z.((p(z, y)) <-> (~(exists x.((p(z, x)) /\ (p(x, z))))))))
(exists x.(p(x))) -> (forall x.(p(x)))
~(forall x.(forall y.((p(x) \/ ~q(x)) /\ (~p(y) \/ q(y)))))