Algebraic numbers in Isabelle/HOL
DOI10.1007/978-3-319-43144-4_24zbMATH Open1478.68443OpenAlexW2400061809MaRDI QIDQ2829274FDOQ2829274
Authors: René Thiemann, Akihisa Yamada 
Publication date: 27 October 2016
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-43144-4_24
Recommendations
- A verified implementation of algebraic numbers in Isabelle/HOL
- A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
- Construction of real algebraic numbers in Coq
- Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
Symbolic computation and algebraic computation (68W30) Algebraic numbers; rings of algebraic integers (11R04) Mechanization of proofs and logical operations (03B35) Formalization of mathematics in connection with theorem provers (68V20) Solving polynomial systems; resultants (13P15)
Cites Work
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Title not available (Why is that?)
- Isabelle/HOL. A proof assistant for higher-order logic
- Polynomials. Translated from the second Russian edition 2001 by Dimitry Leites.
- Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
- The Subresultant PRS Algorithm
- Subresultants and Reduced Polynomial Remainder Sequences
- Data refinement in Isabelle/HOL
- Construction of real algebraic numbers in Coq
- Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials
Cited In (7)
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
- Flexible proof production in an industrial-strength SMT solver
- A verified implementation of algebraic numbers in Isabelle/HOL
- A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
- Classification of finite fields with applications
- On the formalization of Gram-Schmidt process for orthonormalizing a set of vectors
Uses Software
This page was built for publication: Algebraic numbers in Isabelle/HOL
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2829274)
