OK, it looks like we’re not the first people to bang our heads against the ‘what are floating point numbers in formal logic?’ problem… in no particular order, here is what I found via Google Scholar:
- http://smtlib.cs.uiowa.edu/papers/BTRW14.pdf
- https://hal-cea.archives-ouvertes.fr/cea-01795760/document
- https://danliew.co.uk/assets/pdf/Liew-D-2018-PhD-Thesis.pdf
- https://arxiv.org/pdf/1801.00969.pdf
- https://arxiv.org/pdf/1707.02121.pdf
- https://spiral.imperial.ac.uk/bitstream/10044/1/51183/2/klee-n-version-fp-ase-17.pdf
- https://cseweb.ucsd.edu/~dstefan/pubs/andrysco:2018:towards.pdf
- https://par.nsf.gov/servlets/purl/10070275
- https://hal.inria.fr/hal-01314876/document
- https://eprints.soton.ac.uk/416918/1/sbmf.pdf
- https://hal.inria.fr/hal-01522770/document
- https://arxiv.org/pdf/1410.0198.pdf
- http://soarlab.org/publications/popl2017-cbbsgr.pdf
These may give us a good starting point for how to reason over floating point numbers, as well as how to convert them.