A verified implementation of algebraic numbers in Isabelle/HOL

DOI10.1007/s10817-018-09504-wzbMath1468.68326OpenAlexW2904582217WikidataQ90744220 ScholiaQ90744220MaRDI QIDQ2303244

René Thiemann, Akihisa Yamada, Sebastiaan J. C. Joosten

Publication date: 3 March 2020

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-018-09504-w

zbMATH Keywords

resultantstheorem provingreal algebraic geometryalgebraic numbers

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Algebraic numbers; rings of algebraic integers (11R04) Factorization (11Y05) Solving polynomial systems; resultants (13P15) Formalization of mathematics in connection with theorem provers (68V20) Computational real algebraic geometry (14Q30)

Related Items (2)

Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL ⋮ Flexible proof production in an industrial-strength SMT solver

Uses Software

• Isabelle
• Isabelle/HOL
• HOL
• CeTA
• Transfer
• Lifting
• Berlekamp Zassenhaus
• Archive Formal Proofs
• Linear Recurrences
• Count Complex Roots

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On multiset orderings
• Isabelle/HOL. A proof assistant for higher-order logic
• Optimizations of the subresultant algorithm
• A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
• Algebraic Numbers in Isabelle/HOL
• Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
• Construction of Real Algebraic Numbers in Coq
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Termination Competition (termCOMP 2015)
• Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials
• The Subresultant PRS Algorithm
• Data Refinement in Isabelle/HOL
• On Euclid's Algorithm and the Theory of Subresultants

This page was built for publication: A verified implementation of algebraic numbers in Isabelle/HOL