- Here is an updated version of the article describing this work
- The code is collected in this archive : qe_rcf.tgz . Instructions for installation are included in the tarball. Here is a brief overview of the part of this archive which is not contained in the ssreflect 1.3pl2 release:
- zint.v: ssreflect signed integers
- orderedalg.v: ordered integral domains and fields library
- interval.v: interval library
- poly.v / polydiv.v / polyorder.v: a revision of the theory of polynomials
- polyrcf.v: theory of polynomials on real closed fields
- qe_rcf_th.v: establishes the results from section 5 of the paper above.
- ordered_qelim.v: defines the first order language of real closed fields and proves the reduction to the “one existential” case (cf 6.1 6.2.1 and 6.3)
- qe_rcf.v: does the formula transformations (cf 6.2.2) in order to provide dec, which is called ccount_gt0 in here
This page was last updated at
2014-12-01 03:52:16 +0100
