Licensing the Mizar Mathematical Library
From MaRDI portal
Publication:5200114
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
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
Cites Work
