pyprover
pyprover copied to clipboard
Bug in expressions with quantifiers
I have been trying different FOL expressions with quantifiers and equality (Eq
).
Firstly, strict_proves
seems to provide incorrect results for many expressions. For example:
# Expression for testing whether predicate P is true for three or more different constants
>>> strict_proves((P(a)), EX(x, EX(y, EX(z, P(x) & P(y) & P(z) & ~Eq(x,y) & ~Eq(y,z) ))))
True
>>> proves((P(a)), EX(x, EX(y, EX(z, P(x) & P(y) & P(z) & ~Eq(x,y) & ~Eq(y,z) ))))
False
Secondly, proves
gets stuck when given expressions with many nested quantifiers. For example:
# Function gets stuck and never returns
proves((P(a), P(b)), EX(x,EX(y,EX(z, P(x) & P(y) & P(z) & ~Eq(x,y) & ~Eq(y,z)))))