A Decision Procedure for the First Order Theory of Real Addition with Order
Consider the first order theory of the real numbers with the predicates + (plus) and < (less than). Let S be the set of true sentences. We first present an elimination of quantifiers decision procedure for S, and then analyse it to show that it takes at most time 2^2^cn, c a constant, to decide s...
| Main Authors: | , |
|---|---|
| Published: |
2023
|
| Online Access: | https://hdl.handle.net/1721.1/148862 |