A Skeptic's approach to combining HOL and Maple
From MaRDI portal
Publication:1272607
Recommendations
Cited in
(32)- Formally proving size optimality of sorting networks
- Verified interactive computation of definite integrals
- Modelling algebraic structures and morphisms in ACL2
- A reconstruction and extension of Maple's assume facility via constraint contextual rewriting
- Dealing with algebraic expressions over a field in Coq using Maple
- Error analysis of digital filters using HOL theorem proving
- A bi-directional extensible interface between Lean and Mathematica
- Formal proofs of hypergeometric sums. Dedicated to the memory of Andrzej Trybulec
- Proving Valid Quantified Boolean Formulas in HOL Light
- Formal proofs for theoretical properties of Newton's method
- Enabling symbolic and numerical computations in HOL Light
- scientific article; zbMATH DE number 1222427 (Why is no real title available?)
- scientific article; zbMATH DE number 1254246 (Why is no real title available?)
- scientific article; zbMATH DE number 517013 (Why is no real title available?)
- scientific article; zbMATH DE number 1497752 (Why is no real title available?)
- Formal analysis of optical systems
- scientific article; zbMATH DE number 1863375 (Why is no real title available?)
- Interfacing Coq + SSReflect with GAP
- Retargeting OpenAxiom to Poly/ML: towards an integrated proof assistants and computer algebra system framework
- A foundational view on integration problems
- Combining Isabelle and QEPCAD-B in the Prover’s Palette
- A formal proof of the irrationality of (3)
- A certificate-based approach to formally verified approximations
- The control layer in open mechanized reasoning systems: Annotations and tactics
- MBase: Representing knowledge and context for the integration of mathematical software systems
- Formal and efficient primality proofs by use of computer algebra oracles
- Iscalc: An Interactive Symbolic Computation Framework (System Description)
- Hammering Floating-Point Arithmetic
- Comparative verification of the digital library of mathematical functions and computer algebra systems
- Incorporating a database of graphs into a proof assistant
- Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application
- Providing a formal linkage between MDG and HOL
This page was built for publication: A Skeptic's approach to combining HOL and Maple
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1272607)
