Licensing the Mizar Mathematical Library

DOI10.1007/978-3-642-22673-1_11zbMath1278.68290arXiv1107.3212OpenAlexW1667884652WikidataQ57389382 ScholiaQ57389382MaRDI QIDQ5200114

Lionel Elie Mamane, Michael Kohlhase, Piotr Rudnicki, Adam Naumowicz, Jesse Alama, Josef Urban

Publication date: 29 July 2011

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

Full work available at URL: https://arxiv.org/abs/1107.3212

zbMATH Keywords

open dataMizarformal mathematicsfree culturefree licensing

Mathematics Subject Classification ID

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

Related Items

Presentation and manipulation of Mizar properties in an Isabelle object logic, Four decades of {\textsc{Mizar}}. Foreword, Mechanizing complemented lattices within Mizar type system, 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, Mining the Archive of Formal Proofs, Mizar: State-of-the-art and Beyond, Tools for MML Environment Analysis, A learning-based fact selector for Isabelle/HOL, The role of the Mizar mathematical library for interactive proof development in Mizar, Flexary connectives in Mizar, From LCF to Isabelle/HOL, Accessing the Mizar Library with a Weakly Strict Mizar Parser, Enhancement of Mizar Texts with Transitivity Property of Predicates, Finite Groups Representation Theory with Coq, SAT-Enhanced Mizar Proof Checking

Uses Software

• MPTP 0.2
• Mizar
• MML
• Automath

Cites Work

• MPTP 0.2: Design, implementation, and initial experiments
• Evaluation of Automated Theorem Proving on the Mizar Mathematical Library
• Types for Proofs and Programs
• Unnamed Item
• Unnamed Item