Dealing with algebraic expressions over a field in Coq using Maple
From MaRDI portal
Publication:2456560
DOI10.1016/J.JSC.2004.12.004zbMATH Open1126.68101OpenAlexW2013201201MaRDI QIDQ2456560FDOQ2456560
Authors: David Delahaye, Micaela Mayero 
Publication date: 19 October 2007
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jsc.2004.12.004
Recommendations
- Quantifier elimination over algebraically closed fields in a proof assistant using a computer algebra system
- scientific article; zbMATH DE number 1863375
- Construction of real algebraic numbers in Coq
- Interfacing Coq + SSReflect with GAP
- Implementing the cylindrical algebraic decomposition within the Coq system
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- \(\Omega\)\textsc{mega}: towards a mathematical assistant
- A Skeptic's approach to combining HOL and Maple
- Theorem proving modulo
- Proof by computation in the Coq system
- On the role of OpenMath in interactive mathematical documents
- Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants
- Title not available (Why is that?)
- Autarkic computations in formal proofs
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
Cited In (10)
- Towards the formal specification and verification of Maple programs
- Retargeting OpenAxiom to Poly/ML: towards an integrated proof assistants and computer algebra system framework
- A foundational view on integration problems
- Theorem Proving in Higher Order Logics
- A formal proof of the irrationality of \(\zeta(3)\)
- A simple canonical representation of rational numbers
- Interfacing Coq + SSReflect with GAP
- A bi-directional extensible interface between Lean and Mathematica
- Quantifier elimination over algebraically closed fields in a proof assistant using a computer algebra system
- Domains and expressions: an interface between two approaches to computer algebra
Uses Software
This page was built for publication: Dealing with algebraic expressions over a field in Coq using Maple
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2456560)
