A verified implementation of algebraic numbers in Isabelle/HOL (Q2303244): Difference between revisions

@@ Property / DOI @@
-.1007/s10817-018-09504-w
@@ Property / DOI: 10.1007/s10817-018-09504-w / rank @@
-Normal rank
@@ Property / describes a project that uses @@
+Transfer
@@ Property / describes a project that uses: Transfer / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Lifting
@@ Property / describes a project that uses: Lifting / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Berlekamp Zassenhaus
@@ Property / describes a project that uses: Berlekamp Zassenhaus / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CeTA
@@ Property / describes a project that uses: CeTA / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Archive Formal Proofs
@@ Property / describes a project that uses: Archive Formal Proofs / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL
@@ Property / describes a project that uses: HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Count Complex Roots
@@ Property / describes a project that uses: Count Complex Roots / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Linear Recurrences
@@ Property / describes a project that uses: Linear Recurrences / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10817-018-09504-w
+Normal rank
@@ Property / OpenAlex ID @@
+W2904582217
@@ Property / OpenAlex ID: W2904582217 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5277869
@@ Property / cites work: Q5277869 / rank @@
+Normal rank
@@ Property / cites work @@
+The Subresultant PRS Algorithm
@@ Property / cites work: The Subresultant PRS Algorithm / rank @@
+Normal rank
@@ Property / cites work @@
+On Euclid's Algorithm and the Theory of Subresultants
+Normal rank
@@ Property / cites work @@
+Construction of Real Algebraic Numbers in Coq
@@ Property / cites work: Construction of Real Algebraic Numbers in Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
+Normal rank
@@ Property / cites work @@
+A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
+Normal rank
@@ Property / cites work @@
+Optimizations of the subresultant algorithm
@@ Property / cites work: Optimizations of the subresultant algorithm / rank @@
+Normal rank
@@ Property / cites work @@
+Q4406533
@@ Property / cites work: Q4406533 / rank @@
+Normal rank
@@ Property / cites work @@
+Termination Competition (termCOMP 2015)
@@ Property / cites work: Termination Competition (termCOMP 2015) / rank @@
+Normal rank
@@ Property / cites work @@
+Data Refinement in Isabelle/HOL
@@ Property / cites work: Data Refinement in Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+On multiset orderings
@@ Property / cites work: On multiset orderings / rank @@
+Normal rank
@@ Property / cites work @@
+Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials
+Normal rank
@@ Property / cites work @@
+Q4282674
@@ Property / cites work: Q4282674 / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Q3232347
@@ Property / cites work: Q3232347 / rank @@
+Normal rank
@@ Property / cites work @@
+Algebraic Numbers in Isabelle/HOL
@@ Property / cites work: Algebraic Numbers in Isabelle/HOL / rank @@
+Normal rank
@@ Property / DOI @@
+.1007/S10817-018-09504-W
@@ Property / DOI: 10.1007/S10817-018-09504-W / rank @@
+Normal rank