Certified Computer Algebra on Top of an Interactive Theorem Prover

DOI10.1007/978-3-540-73086-6_8MaRDI QIDQ5428262zbMATH OpenOpenAlexWikidataFDO

Authors Cezary Kaliszyk, Freek Wiedijk

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

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30)

Recommendations

• scientific article; zbMATH DE number 1497749
• Algebraic methods for interactive proof systems
• scientific article; zbMATH DE number 5899421
• scientific article; zbMATH DE number 1863375
• scientific article; zbMATH DE number 1222427
• scientific article; zbMATH DE number 1389647
• Integrating computer algebra into proof planning
• scientific article; zbMATH DE number 4108029
• Computer-assisted proofs in analysis
• Computerized proof techniques for undergraduates

Cited in

(20)

• A Skeptic's approach to combining HOL and Maple
• The natural algorithmic approach of mixed trigonometric-polynomial problems
• Modelling algebraic structures and morphisms in ACL2
• A bi-directional extensible interface between Lean and Mathematica
• Interfacing computer algebra and deduction systems via the logic broker architecture
• Enabling symbolic and numerical computations in HOL Light
• scientific article; zbMATH DE number 1262431 (Why is no real title available?)
• scientific article; zbMATH DE number 517013 (Why is no real title available?)
• scientific article; zbMATH DE number 1497749 (Why is no real title available?)
• scientific article; zbMATH DE number 1538012 (Why is no real title available?)
• Formal analysis of optical systems
• scientific article; zbMATH DE number 1389645 (Why is no real title available?)
• Proof assistant decision procedures for formalizing origami
• View of computer algebra data from Coq
• High-Level Theories
• Automating Side Conditions in Formalized Partial Functions
• Combining Isabelle and QEPCAD-B in the Prover’s Palette
• Comparative verification of the digital library of mathematical functions and computer algebra systems
• An interpreter for quantum circuits
• Implementing geometric algebra products with binary trees

Describes a project that uses

Uses Software

• Coq
• Isabelle
• Maple
• Mathematica
• HOL Light
• REDLOG

This page was built for publication: Certified Computer Algebra on Top of an Interactive Theorem Prover

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5428262)