Specification and integration of theorem provers and computer algebra systems

DOI10.1007/BFB0055905MaRDI QIDQ4217952zbMATH OpenFDO

Authors Jacques Calmet, Karsten Homann, Fausto Giunchiglia, Piergiorgio Bertoli

Publication date 19 April 1999

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BFB0055905

zbMATH Keywords

automated theorem proverscomputer algebra systems

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30)

Recommendations

• scientific article; zbMATH DE number 1389647
• Integrating computer algebra into proof planning
• scientific article; zbMATH DE number 1863375
• A Skeptic's approach to combining HOL and Maple

Cited in

(10)

• Integrating computer algebra into proof planning
• Interfacing computer algebra and deduction systems via the logic broker architecture
• scientific article; zbMATH DE number 1497752 (Why is no real title available?)
• scientific article; zbMATH DE number 1389647 (Why is no real title available?)
• Integrating systems around the user: combining Isabelle, Maple, and QEPCAD in the prover's palette
• Retargeting OpenAxiom to Poly/ML: towards an integrated proof assistants and computer algebra system framework
• A foundational view on integration problems
• Certified Computer Algebra on Top of an Interactive Theorem Prover
• The control layer in open mechanized reasoning systems: Annotations and tactics
• Combined reasoning by automated cooperation

Describes a project that uses

Uses Software

• Isabelle
• OMRS
• Maple

This page was built for publication: Specification and integration of theorem provers and computer algebra systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4217952)