Mathematical Knowledge Management

DOI10.1007/11618027MaRDI QIDQ5898533zbMATH OpenOpenAlexFDO

Authors

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

Mechanization of proofs and logical operations (03B35) Knowledge representation (68T30)

Recommendations

• Faithfully reflecting the structure of informal mathematical proofs into formal type theories
• Mathematical Knowledge Management
• Supporting the formal verification of mathematical texts
• scientific article; zbMATH DE number 2085176
• Foreword to the special focus on formal proofs for mathematics and computer science

Cited in

(7)

• Experiences from exporting major proof assistant libraries
• Faithfully reflecting the structure of informal mathematical proofs into formal type theories
• MathLang Translation to Isabelle Syntax
• scientific article; zbMATH DE number 2085176 (Why is no real title available?)
• The formalization of group theory knowledge and solving
• Simple type theory is not too simple: Grothendieck's schemes without dependent types
• Mathematical Knowledge Management

Describes a project that uses

Uses Software

• Coq
• Isabelle/HOL
• Mizar
• GF

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 Q5898533)