Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (Q1725844): Difference between revisions

@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2745160404
@@ Property / OpenAlex ID: W2745160404 / rank @@
+Normal rank
@@ Property / arXiv ID @@
+.08238
@@ Property / arXiv ID: 1506.08238 / rank @@
+Normal rank
@@ Property / cites work @@
+MetiTarski: An automatic theorem prover for real-valued special functions
+Normal rank
@@ Property / cites work @@
+Algorithms in real algebraic geometry
@@ Property / cites work: Algorithms in real algebraic geometry / rank @@
+Normal rank
@@ Property / cites work @@
+QEPCAD B
@@ Property / cites work: QEPCAD B / rank @@
+Normal rank
@@ Property / cites work @@
+Q5301656
@@ Property / cites work: Q5301656 / rank @@
+Normal rank
@@ Property / cites work @@
+Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
+Normal rank
@@ Property / cites work @@
+Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals
+Normal rank
@@ Property / cites work @@
+A Machine-Checked Proof of the Odd Order Theorem
@@ Property / cites work: A Machine-Checked Proof of the Odd Order Theorem / rank @@
+Normal rank
@@ Property / cites work @@
+Code Generation via Higher-Order Rewrite Systems
@@ Property / cites work: Code Generation via Higher-Order Rewrite Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Verifying Nonlinear Real Formulas Via Sums of Squares
+Normal rank
@@ Property / cites work @@
+A Formal Proof of Cauchy’s Residue Theorem
@@ Property / cites work: A Formal Proof of Cauchy’s Residue Theorem / rank @@
+Normal rank
@@ Property / cites work @@
+Implementing the cylindrical algebraic decomposition within the Coq system
+Normal rank
@@ Property / cites work @@
+Q4282674
@@ Property / cites work: Q4282674 / rank @@
+Normal rank
@@ Property / cites work @@
+Formalization of Bernstein polynomials and applications to global optimization
+Normal rank
@@ Property / cites work @@
+Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Real Algebraic Strategies for MetiTarski Proofs
@@ Property / cites work: Real Algebraic Strategies for MetiTarski Proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Q4779788
@@ Property / cites work: Q4779788 / rank @@
+Normal rank
@@ Property / cites work @@
+A general approach to isolating roots of a bitstream polynomial
+Normal rank
@@ Property / cites work @@
+Cylindrical algebraic decomposition using validated numerics
+Normal rank
@@ Property / cites work @@
+Algebraic Numbers in Isabelle/HOL
@@ Property / cites work: Algebraic Numbers in Isabelle/HOL / rank @@
+Normal rank