evhub / pyprover Goto Github PK

Could you please provide documentation tjat contains detailed examples so that we understand more

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)))))

Thanks for this awesome library. But I think maybe the following results are wrong?

In [4]: from pyprover import *

In [5]: f1 = '∃y,∃z,∀x, (Q(x,z)->Q(y,x))'
   ...: f2 = '∀y,∃x, ((R(x,z)∧R(x))->R(y))'
   ...: print(proves_and_proved_by(expr(f1),expr(f2)))
True

these two are not equal, right?

In [2]: from pyprover import *
   ...: f1 = '∀z,∃x, ¬((Q(z)∧Q(x)))'
   ...: f2 = '∃z,∀x, ¬((Q(x)∧Q(z)))'
   ...: print(proves_and_proved_by(expr(f1),expr(f2)))
True

these two are also not equal, right?

>> x = Var('x')
>> y = Var('y')  

>> (Q(x)).find_unification(Q(a))
>> {Var("x"): Const("a")}

>> (Q(x) & P(y)).find_unification((Q(a) & P(b)))
>> 

That is, (Q(x) & P(y)).find_unification((Q(a) & P(b))) output None.

I think there is something wrong with the find_unification.

Is it possible to use this library to create Fitch-style natural deduction or semantic tableaux tree diagrams?