A Skeptic's approach to combining HOL and Maple
From MaRDI portal
Publication:1272607
DOI10.1023/A:1006023127567zbMath0916.68142OpenAlexW1525737662MaRDI QIDQ1272607
Publication date: 3 January 1999
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1023/a:1006023127567
Analysis of algorithms and problem complexity (68Q25) Symbolic computation and algebraic computation (68W30)
Related Items
Formal proofs of hypergeometric sums. Dedicated to the memory of Andrzej Trybulec, Enabling Symbolic and Numerical Computations in HOL Light, Formal and efficient primality proofs by use of computer algebra oracles, Providing a formal linkage between MDG and HOL, Unnamed Item, A bi-directional extensible interface between Lean and Mathematica, Formally proving size optimality of sorting networks, Unnamed Item, Formal analysis of optical systems, A reconstruction and extension of Maple's assume facility via constraint contextual rewriting, Dealing with algebraic expressions over a field in Coq using Maple, A certificate-based approach to formally verified approximations, Error analysis of digital filters using HOL theorem proving, Interfacing Coq + SSReflect with GAP, The control layer in open mechanized reasoning systems: Annotations and tactics, MBase: Representing knowledge and context for the integration of mathematical software systems, Retargeting OpenAxiom to Poly/ML: Towards an Integrated Proof Assistants and Computer Algebra System Framework, A Foundational View on Integration Problems, Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application, Proving Valid Quantified Boolean Formulas in HOL Light, Verified interactive computation of definite integrals, Formal proofs for theoretical properties of Newton's method, Combining Isabelle and QEPCAD-B in the Prover’s Palette, Modelling algebraic structures and morphisms in ACL2
Uses Software
