计算一阶算术公式

Question

是否有一个python包用于计算有界的一阶算术公式？你知道吗

例如，它得到一个有界的一阶算术表达式

>>> exp = 'forall x < z exists y < x ((2 * y + 1 = x) or (2 * y = x))'

自由变量z的值

>>> tau = [(z,20)]

并返回其值

>>> eval(exp, tau)  
False 

Answer 1

也许你要找的是所谓的“量词消除”。如果是这样的话，看看QEPCAD。[1] 为QEPCAD创建Python接口可能比找到Python实现更容易。你知道吗

[1]http://www.usna.edu/CS/~qepcad/B/QEPCAD.html