hex
hex
Table of Contents
1.
HexBasic: shared dependency-free utilities
2.
HexArith: low-level arithmetic foundations
3.
HexPrimality: certified primality at scale
4.
HexPoly: normalized dense polynomials
5.
HexMvPoly: executable sparse multivariate polynomials
6.
HexSparsePoly: sparse univariate polynomials
7.
HexModArith: machine-word modular arithmetic
8.
HexPolyFp: prime-field dense polynomials
9.
HexPolyZ: integer dense polynomials
10.
HexGFqRing: executable Fₚ quotient ring
11.
HexHensel: executable Hensel lifting
12.
HexRoots: certified complex-root isolation
13.
HexRealRoots: certified real-root isolation
14.
HexRCF: a decision procedure for univariate real arithmetic
15.
HexMatrix: dense matrices and arithmetic
16.
HexRowReduce: Gauss-Jordan reduction, span, and nullspace
17.
HexBerlekamp: factorization over finite fields
18.
HexGF2: packed GF(2) polynomials and GF(2ⁿ) fields
19.
HexGFqField: executable GF(pⁿ)
20.
HexConway: verified Conway-polynomial lookup
21.
HexGFq: canonical finite-field constructors
22.
HexDeterminant: the Leibniz determinant and cofactor theory
23.
HexBareiss: the fraction-free determinant
24.
HexResultant: subresultants and discriminants
25.
HexGramSchmidt: Gram-Schmidt orthogonalization
26.
HexLLL: lattice basis reduction
27.
HexBerlekampZassenhaus: factorization over the integers
28.
factor_poly
and
irreducibility
: certified factoring
29.
HexNumberField: exact algebraic numbers
30.
HexNumberFieldTower: successive algebraic extensions
31.
HexPermGroup: checked finite permutation groups
32.
HexGraphIso: coloured graph canonical labelling
33.
The
nauty
canonical labelling algorithm
34.
Tutorials
35.
Draft sections for unreleased libraries
14.
HexRCF: a decision procedure for univariate real arithmetic
14.1.
Introduction
14.2.
The four quantifier forms
14.3.
Polynomial and rational syntax
14.4.
False sentences and fall-through
14.5.
Rewriting other interval conventions
14.6.
Sentences as data
14.7.
Performance
14.8.
Certificates and what the kernel checks
14.9.
Cross-references
←
13.8. Cross-references
14.1. Introduction
→
14. HexRCF: a decision procedure for univariate real arithmetic
🔗
14.1.
Introduction
14.2.
The four quantifier forms
14.3.
Polynomial and rational syntax
14.4.
False sentences and fall-through
14.5.
Rewriting other interval conventions
14.6.
Sentences as data
14.7.
Performance
14.8.
Certificates and what the kernel checks
14.9.
Cross-references
←
13.8. Cross-references
14.1. Introduction
→