There is nothing inherently difficult about practical implementations of continuous numbers for automated reasoning compared to more discrete mathematical struc

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.pdf 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 https://shemesh.larc.nasa.gov/fm/papers/nfm2019-draft.pdf Z3 also supports real theories: https://smt-lib.org/theories-Reals.shtml https://smt-lib.org/theories-Reals.shtml