Integrating computer algebra into proof planning
From MaRDI portal
Publication:1272609
Recommendations
- Proof planning: A practical approach to mechanized reasoning in mathematics
- An integral theorem prover and the role of proof planning
- Specification and integration of theorem provers and computer algebra systems
- scientific article; zbMATH DE number 1389647
- Computer algebra meets automated theorem proving: Integrating Maple and PVS
- scientific article; zbMATH DE number 5899421
- Non-trivial symbolic computations in proof planning
- scientific article; zbMATH DE number 4108029
- Computer-assisted proofs in analysis
- Integrating constraint solving into proof planning
Cited in
(26)- An integral theorem prover and the role of proof planning
- A Skeptic's approach to combining HOL and Maple
- Comparing approaches to the exploration of the domain of residue classes.
- Knowledge-based proof planning
- Integrating searching and authoring in Mizar
- A bi-directional extensible interface between Lean and Mathematica
- Proof planning: A practical approach to mechanized reasoning in mathematics
- Interfacing computer algebra and deduction systems via the logic broker architecture
- Specification and integration of theorem provers and computer algebra systems
- Classifying isomorphic residue classes
- scientific article; zbMATH DE number 1497744 (Why is no real title available?)
- Integrating constraint solving into proof planning
- Non-trivial symbolic computations in proof planning
- Computer algebra meets automated theorem proving: Integrating Maple and PVS
- Inductive theorem proving and computer algebra in the MathWeb Software Bus
- scientific article; zbMATH DE number 1389645 (Why is no real title available?)
- scientific article; zbMATH DE number 1389647 (Why is no real title available?)
- Retargeting OpenAxiom to Poly/ML: towards an integrated proof assistants and computer algebra system framework
- \(\Omega\)\textsc{mega}: towards a mathematical assistant
- Mathematical Knowledge Management
- Certified Computer Algebra on Top of an Interactive Theorem Prover
- Combining Isabelle and QEPCAD-B in the Prover’s Palette
- MBase: Representing knowledge and context for the integration of mathematical software systems
- Formal and efficient primality proofs by use of computer algebra oracles
- Types, Tableaus and Gödel’s God in Isabelle/HOL
- Combined reasoning by automated cooperation
This page was built for publication: Integrating computer algebra into proof planning
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1272609)
