Integrating computer algebra into proof planning

DOI10.1023/A:1006059810729zbMATH Open0916.68144OpenAlexW1881765559MaRDI QIDQ1272609FDOQ1272609

Authors: Manfred Kerber, Michael Kohlhase, Volker Sorge 

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:1006059810729

Recommendations

• Proof planning: A practical approach to mechanized reasoning in mathematics
• An integral theorem prover and the role of proof planning
• scientific article; zbMATH DE number 1222427
• Publication:4934140
• scientific article; zbMATH DE number 1863375
• scientific article; zbMATH DE number 5899421
• scientific article; zbMATH DE number 1538012
• scientific article; zbMATH DE number 4108029
• Computer-assisted proofs in analysis
• scientific article; zbMATH DE number 1538007

zbMATH Keywords

computer algebra systemsmechanized reasoning systems

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30)

Cited In (22)

• Title not available (Why is that?)
• Title not available (Why is that?)
• Retargeting OpenAxiom to Poly/ML: towards an integrated proof assistants and computer algebra system framework
• Title not available (Why is that?)
• Interfacing computer algebra and deduction systems via the logic broker architecture
• MBase: Representing knowledge and context for the integration of mathematical software systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Formal and efficient primality proofs by use of computer algebra oracles
• Combined reasoning by automated cooperation
• Comparing approaches to the exploration of the domain of residue classes.
• Title not available (Why is that?)
• Knowledge-based proof planning
• Title not available (Why is that?)
• Proof planning: A practical approach to mechanized reasoning in mathematics
• Mathematical Knowledge Management
• Certified Computer Algebra on Top of an Interactive Theorem Prover
• Combining Isabelle and QEPCAD-B in the Prover’s Palette
• A bi-directional extensible interface between Lean and Mathematica
• An integral theorem prover and the role of proof planning
• Integrating searching and authoring in Mizar
• \(\Omega\)\textsc{mega}: towards a mathematical assistant

Uses Software

• AXIOM
• Mathematica
• MuPAD
• REDUCE
• OMRS
• Nuprl
• Analytica

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)