18. HexRCF: a decision procedure for univariate real arithmetic🔗

1. 18.1. Introduction
2. 18.2. The four quantifier forms
3. 18.3. Polynomial and rational syntax
4. 18.4. False sentences and fall-through
5. 18.5. Rewriting other interval conventions
6. 18.6. Sentences as data
7. 18.7. Performance
8. 18.8. Certificates and what the kernel checks
9. 18.9. Algebraic coefficients
10. 18.10. Simultaneous signs and repeated roots over a cubic field
11. 18.11. Arithmetic at a selected algebraic root
12. 18.12. Signs and selected roots with BKR
13. 18.13. Specialization and ordinary real enclosures
14. 18.14. Ordinary samples over a selected field
15. 18.15. Native sample coefficient conversion
16. 18.16. Selected coefficient identities at one real reader
17. 18.17. Complete checked cells in an ordinary real model
18. 18.18. Frozen cells over a selected algebraic coefficient
19. 18.19. Ordinary witnesses from one infinitesimal replay
20. 18.20. A frozen row at an ordinary selected root
21. 18.21. Quoting a supplied root replay
22. 18.22. An ordinary real root over a selected field
23. 18.23. Caller-supplied finite bounds
24. 18.24. Cross-references