Certified Computer Algebra on Top of an Interactive Theorem Prover
From MaRDI portal
Publication:5428262
DOI10.1007/978-3-540-73086-6_8zbMath1202.68382OpenAlexW1569069553WikidataQ108482198 ScholiaQ108482198MaRDI QIDQ5428262
Freek Wiedijk, Cezary Kaliszyk
Publication date: 28 November 2007
Published in: Towards Mechanized Mathematical Assistants (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-73086-6_8
Related Items (11)
Enabling Symbolic and Numerical Computations in HOL Light ⋮ A bi-directional extensible interface between Lean and Mathematica ⋮ Formal analysis of optical systems ⋮ The natural algorithmic approach of mixed trigonometric-polynomial problems ⋮ Proof Assistant Decision Procedures for Formalizing Origami ⋮ View of Computer Algebra Data from Coq ⋮ Implementing geometric algebra products with binary trees ⋮ High-Level Theories ⋮ Automating Side Conditions in Formalized Partial Functions ⋮ Combining Isabelle and QEPCAD-B in the Prover’s Palette ⋮ Modelling algebraic structures and morphisms in ACL2
Uses Software
This page was built for publication: Certified Computer Algebra on Top of an Interactive Theorem Prover
