| ▲ | thesmtsolver 6 hours ago | |
There is nothing inherently difficult about practical implementations of continuous numbers for automated reasoning compared to more discrete mathematical structures. They are handleable by standard FOL itself. See ACL2's support for floating point arithmetic. https://www.cs.utexas.edu/~moore/publications/double-float.p... SMT solvers also support real number theories: https://shemesh.larc.nasa.gov/fm/papers/nfm2019-draft.pdf Z3 also supports real theories: | ||