Mathematical Knowledge Management

DOI10.1007/11618027MaRDI QIDQ5898511zbMATH OpenOpenAlexFDO

Authors Adam Grabowski, Christoph Schwarzweller

Publication date 12 February 2007

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

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

Mathematics Subject Classification ID

Knowledge representation (68T30)

Recommendations

• scientific article; zbMATH DE number 1951626
• MBase: Representing knowledge and context for the integration of mathematical software systems
• Mathematical Knowledge Management
• Using and parsing the Mizar language
• The Mizar Mathematical Library in OMDoc: translation and applications

Cited in

(18)

• Flexary connectives in Mizar
• Formalization of quasilattices
• On weakly associative lattices and near lattices
• Splitting fields
• Four decades of \textsc{Mizar}. Foreword
• Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization
• Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver
• Improving legibility of formal proofs based on the close reference principle is NP-hard
• scientific article; zbMATH DE number 5607884 (Why is no real title available?)
• scientific article; zbMATH DE number 5124871 (Why is no real title available?)
• Mizar: state-of-the-art and beyond
• On duplication in mathematical repositories
• scientific article; zbMATH DE number 2078371 (Why is no real title available?)
• Multidimensional measure space and integration
• Elementary number theory problems. XII: Primes in arithmetic progression
• Simple extensions
• Symmetrical piecewise linear functions composed by absolute value function
• Formalization of trellises and tolerance relations

Describes a project that uses

Uses Software

• IsaWin
• Isar
• Mizar

This page was built for publication: Mathematical Knowledge Management

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