Isabelle import infrastructure for the Mizar Mathematical Library

DOI10.1007/978-3-319-96812-4_13MaRDI QIDQ1798961zbMATH OpenOpenAlexWikidataFDO

Authors Cezary Kaliszyk, Karol Pąk

Publication date 18 October 2018

Full work available at URL https://doi.org/10.1007/978-3-319-96812-4_13

Mathematics Subject Classification ID

Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.) (68U35)

Recommendations

• A new export of the Mizar mathematical library
• Semantics of Mizar as an Isabelle object logic
• The Mizar Mathematical Library in OMDoc: translation and applications
• A comparison of Mizar and Isar
• The role of the Mizar mathematical library for interactive proof development in Mizar

Cited in

(6)

• Presentation and manipulation of Mizar properties in an Isabelle object logic
• A new export of the Mizar mathematical library
• Declarative Proof Translation (Short Paper)
• mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library
• Semantics of Mizar as an Isabelle object logic
• Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.

Describes a project that uses

Uses Software

• HOL Light
• Mizar
• MPTP 0.2
• Isabelle/HOL
• Isabelle

This page was built for publication: Isabelle import infrastructure for the Mizar Mathematical Library

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