Using Open Mathematical Documents to Interface Computer Algebra and Proof Assistant Systems

DOI10.1007/978-3-642-02614-0_37MaRDI QIDQ3637304zbMATH OpenOpenAlexFDO

Authors Jónathan Heras, Vico Pascual, Julio Rubio

Publication date 9 July 2009

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

Full work available at URL https://doi.org/10.1007/978-3-642-02614-0_37

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Knowledge representation (68T30)

Recommendations

• On the role of OpenMath in interactive mathematical documents
• scientific article; zbMATH DE number 1497742
• Interactive Mathematical Documents
• Certified and portable mathematical documents from formal contexts
• scientific article; zbMATH DE number 2079831

Cites work

• scientific article; zbMATH DE number 3264757 (Why is no real title available?)
• Interoperating between computer algebra systems: computing homology of groups with Kenzo and GAP
• Mediated Access to Symbolic Computation Systems

Cited in

(11)

• Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants
• fKenzo: a user interface for computations in algebraic topology
• On the role of OpenMath in interactive mathematical documents
• The freedom to extend OpenMath and its utility
• Semantic preserving bijective mappings of mathematical formulae between document preparation systems and computer algebra systems
• Proving with ACL2 the correctness of simplicial sets in the Kenzo system
• Mathematical Knowledge Management
• scientific article; zbMATH DE number 2079831 (Why is no real title available?)
• Integrating semantic mathematical documents and dynamic notebooks
• Abramowitz and Stegun – A Resource for Mathematical Document Analysis
• Comparative verification of the digital library of mathematical functions and computer algebra systems

Describes a project that uses

Uses Software

• OMDoc
• HAP
• Kenzo
• GAP
• ACL2

This page was built for publication: Using Open Mathematical Documents to Interface Computer Algebra and Proof Assistant Systems

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