scientific article; zbMATH DE number 2079831

MaRDI QIDQ4471938zbMATH OpenFDO

Authors Michael Kohlhase

Publication date 30 July 2004

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/1930/19300032.htm

Mathematics Subject Classification ID

General and miscellaneous specific topics (00A99) Knowledge representation (68T30) Symbolic computation and algebraic computation (68W30) Problem books, competitions, examinations (aspects of mathematics education) (97U40) Technological tools, calculators (aspects of mathematics education) (97U70)

Recommendations

• On the role of OpenMath in interactive mathematical documents
• The Mizar Mathematical Library in OMDoc: translation and applications
• scientific article; zbMATH DE number 1951636
• scientific article; zbMATH DE number 2151209
• Exchange of mathematical information on the web: Present and future
• Using Open Mathematical Documents to Interface Computer Algebra and Proof Assistant Systems
• On the road to a comprehensive open digital mathematics library
• scientific article; zbMATH DE number 1961549

Cited in

(16)

• Proof assistants: history, ideas and future
• Knowledge representation and management in ACTIVEMATH
• OMDoc
• Student proof exercises using MathsTiles and Isabelle/HOL in an intelligent book
• Checking content consistency of integrated web documents
• scientific article; zbMATH DE number 1574466 (Why is no real title available?)
• Communication protocols for mathematical services based on KQML and OMRS
• Web interfaces for proof assistants
• \textsc{Plat}{\(\Omega\)}: a mediator between text-editors and proof assistance systems
• Unifying Math Ontologies: A Tale of Two Standards
• Using Open Mathematical Documents to Interface Computer Algebra and Proof Assistant Systems
• scientific article; zbMATH DE number 1951631 (Why is no real title available?)
• Authoring LeActiveMath Calculus Content
• MBase: Representing knowledge and context for the integration of mathematical software systems
• Realization of an OpenMath server for REDUCE
• Innovations in computational type theory using Nuprl

Describes a project that uses

Uses Software

• GAP
• CoFI
• OMRS
• MBase
• PROSPER

This page was built for publication:

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