Mathematical knowledge management in HELM

DOI10.1023/A:1022907629104MaRDI QIDQ1810904zbMATH OpenOpenAlexFDO

Authors Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen, Ferruccio Guidi, Irene Schena

Publication date 9 June 2003

Published in Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/a:1022907629104

zbMATH Keywords

XMLCoqformal mathematicsmathematical knowledge managementMathMLXSLTHELM

Mathematics Subject Classification ID

Knowledge representation (68T30)

Recommendations

• Mathematical knowledge management in HELM
• scientific article; zbMATH DE number 1863377
• scientific article; zbMATH DE number 2078376
• From G.H.H. and Littlewood to XML and Maple: changing needs and expectations in mathematical knowledge management
• Towards MKM in the large: modular representation and scalable software architecture

Cited in

(25)

• From G.H.H. and Littlewood to XML and Maple: changing needs and expectations in mathematical knowledge management
• Mathematical knowledge management in HELM
• User interaction with the Matita proof assistant
• Math Literate Knowledge Management via Induced Material
• Mathematical knowledge management: MKM 2001. Electronic proceedings of the 1st international workshop, RISC, Schloß Hagenberg, Austria, September 24--26, 2001
• scientific article; zbMATH DE number 1951635 (Why is no real title available?)
• A Logically Saturated Extension of ${{\bar\lambda\mu\tilde{\mu}}}$
• A user interface for a mathematical system that allows ambiguous formulae
• View of computer algebra data from Coq
• Combining source, content, presentation, narration, and relational representation
• From G. H. H. and Littlewood to XML and Maple: Changing needs and expectations in mathematical knowledge management
• Merging Procedural and Declarative Proof
• Mathematical Knowledge Management
• Towards MKM in the large: modular representation and scalable software architecture
• \textit{Theorema}: Towards computer-aided mathematical theory exploration
• scientific article; zbMATH DE number 1951628 (Why is no real title available?)
• Crystal: Integrating structured queries into a tactic language
• Procedural representation of CIC proof terms
• Innovations in computational type theory using Nuprl
• scientific article; zbMATH DE number 2078376 (Why is no real title available?)
• Mathematical Knowledge Management
• scientific article; zbMATH DE number 1951636 (Why is no real title available?)
• Formal Reasoning Using Distributed Assertions
• A fine-tuning retrieval system for mathematical information
• scientific article; zbMATH DE number 1863377 (Why is no real title available?)

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Mathematical knowledge management in HELM

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