CODEWITHSUNDEEP
pythonmathlogicpackagearithmetic-expressions
Kaveh
Kaveh

Reputation: 466

Evaluating first-order arithmetic formulas

Is there a python package for evaluating bounded first-order arithmetic formulas?

For example, it gets a bounded first-order arithmetic expression

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

and a value for the free variable z

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

and returns its value

>>> eval(exp, tau)  
False

Upvotes: 1

Views: 93

Answers (1)

Robert Dodier
Robert Dodier

Reputation: 17576

Maybe what you are looking for is something called "quantifier elimination". If so, take a look at QEPCAD. [1] It may be easier to create a Python interface for QEPCAD than to find a Python implementation.

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

Upvotes: 1

Related Questions