python - 评估一阶算术公式

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 接口(interface)可能比寻找 Python 实现更容易。

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