Algebraic Numbers in Isabelle/HOL

MaRDI QIDQ7361619FDO

Authors René Thiemann, Akihisa Yamada, Sebastiaan J. C. Joosten, Manuel Eberl

Publication date 22 December 2015

Cites work

• Arctic Termination ...Below Zero
• Certification of complexity proofs using CeTA
• Certification of Termination Proofs Using CeTA
• From Matrix Interpretations over the Rationals to Matrix Interpretations over the Naturals
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Matrix interpretations for proving termination of term rewriting
• Matrix Theory
• Theory of algebraic numbers. Vol. 1

Cited in

(8)

• Complex Lattices, Elliptic Functions, and the Modular Group
• Linear Recurrences
• A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
• A verified LLL algorithm
• Factorization of Polynomials with Algebraic Coefficients
• The BKR Decision Procedure for Univariate Real Arithmetic
• Solving Cubic and Quartic Equations
• The Hermite–Lindemann–Weierstraß Transcendence Theorem

This page was built for software: Algebraic Numbers in Isabelle/HOL