Algebraic numbers in Isabelle/HOL

DOI10.1007/978-3-319-43144-4_24MaRDI QIDQ2829274zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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)

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

Cites work

• scientific article; zbMATH DE number 3750146 (Why is no real title available?)
• Construction of real algebraic numbers in Coq
• Data refinement in Isabelle/HOL
• Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
• Isabelle/HOL. A proof assistant for higher-order logic
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Polynomials. Translated from the second Russian edition 2001 by Dimitry Leites.
• Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials
• Subresultants and Reduced Polynomial Remainder Sequences
• The Subresultant PRS Algorithm

Cited in

(8)

• 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
• Targeting completeness: automated complexity analysis of integer programs

Describes a project that uses

Uses Software

• Lifting
• Transfer
• HOL
• Isabelle/HOL
• Isabelle

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)