stepchowfun / theorem-prover Goto Github PK

Thank you for this useful program.

Is there a way to represent formulas with uniqueness quantifier such as ∃!xP(x) ≡ ∃x(P(x)∧∀y(P(y)→y=x))?

The program finds a proof for

(forall x. forsome y. P(x,y)) implies (forsome y. forall x. P(x,y))

When starting main.py with Python 3.4 on Windows 8 I get a syntax error:

File "C:...\main.py", line 355
print "First-Order Logic Theorem Prover"
^
SyntaxError: invalid syntax

When i try to run the "forall x. P(x) implies (Q(x) implies P(x))" example i get multiple errors , do you know why that could be ?

There's an information in readme there are some unprovable formulae that will cause this program to loop forever and it is said that's the consequence of Gödel's first incompleteness theorem. I belive that it is rather connected to Church incompletness theorem from 1936 (http://en.wikipedia.org/wiki/Entscheidungsproblem).

The input

(forsome x. forsome y. P(x, y)) implies (forsome y. forsome x. P (x, y))

seems to send the prover into a loop.