Pages that link to "Item:Q2881068"
From MaRDI portal
The following pages link to Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination (Q2881068):
Displaying 21 items.
- Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems (Q287269) (← links)
- Elementary recursive quantifier elimination based on Thom encoding and sign determination (Q529166) (← links)
- Formalization of the arithmetization of Euclidean plane geometry and applications (Q1640646) (← links)
- Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq (Q1725841) (← links)
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (Q1725844) (← links)
- Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem (Q2069874) (← links)
- Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL (Q2303242) (← links)
- A verified implementation of algebraic numbers in Isabelle/HOL (Q2303244) (← links)
- Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants (Q2331077) (← links)
- Formalization of Bernstein polynomials and applications to global optimization (Q2351165) (← links)
- Theorem of three circles in Coq (Q2351412) (← links)
- Algebraic Numbers in Isabelle/HOL (Q2829274) (← links)
- Quantifier elimination over algebraically closed fields in a proof assistant using a computer algebra system (Q2852041) (← links)
- Real Algebraic Strategies for MetiTarski Proofs (Q2907335) (← links)
- (Q3384907) (← links)
- Recent Advances in Real Geometric Reasoning (Q3452275) (← links)
- Formal Global Optimisation with Taylor Models (Q3613424) (← links)
- Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis (Q5048989) (← links)
- Validating Mathematical Structures (Q5048998) (← links)
- Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. (Q5875415) (← links)
- Verified Quadratic Virtual Substitution for Real Arithmetic (Q6488467) (← links)