Pages that link to "Item:Q1272607"
From MaRDI portal
The following pages link to A Skeptic's approach to combining HOL and Maple (Q1272607):
Displaying 26 items.
- Formal proofs of hypergeometric sums. Dedicated to the memory of Andrzej Trybulec (Q286798) (← links)
- Formal analysis of optical systems (Q475384) (← links)
- Formal and efficient primality proofs by use of computer algebra oracles (Q597112) (← links)
- Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application (Q736916) (← links)
- Providing a formal linkage between MDG and HOL (Q878110) (← links)
- Formally proving size optimality of sorting networks (Q1694569) (← links)
- Verified interactive computation of definite integrals (Q2055881) (← links)
- Modelling algebraic structures and morphisms in ACL2 (Q2349534) (← links)
- A reconstruction and extension of Maple's assume facility via constraint contextual rewriting (Q2456557) (← links)
- Dealing with algebraic expressions over a field in Coq using Maple (Q2456560) (← links)
- Error analysis of digital filters using HOL theorem proving (Q2475434) (← links)
- A bi-directional extensible interface between Lean and Mathematica (Q2673306) (← links)
- Proving Valid Quantified Boolean Formulas in HOL Light (Q3088006) (← links)
- Formal proofs for theoretical properties of Newton's method (Q3094171) (← links)
- Enabling Symbolic and Numerical Computations in HOL Light (Q3453133) (← links)
- (Q4499163) (← links)
- Interfacing Coq + SSReflect with GAP (Q5170233) (← links)
- Retargeting OpenAxiom to Poly/ML: Towards an Integrated Proof Assistants and Computer Algebra System Framework (Q5200105) (← links)
- A Foundational View on Integration Problems (Q5200111) (← links)
- Combining Isabelle and QEPCAD-B in the Prover’s Palette (Q5505513) (← links)
- (Q5856420) (← links)
- A certificate-based approach to formally verified approximations (Q5875414) (← links)
- The control layer in open mechanized reasoning systems: Annotations and tactics (Q5950930) (← links)
- MBase: Representing knowledge and context for the integration of mathematical software systems (Q5950933) (← links)
- Comparative verification of the digital library of mathematical functions and computer algebra systems (Q6535563) (← links)
- Incorporating a database of graphs into a proof assistant (Q6648164) (← links)