Presentation and manipulation of Mizar properties in an Isabelle object logic
From MaRDI portal
Publication:2364678
DOI10.1007/978-3-319-62075-6_14zbMath1367.68250OpenAlexW2734056180WikidataQ108482130 ScholiaQ108482130MaRDI QIDQ2364678
Publication date: 21 July 2017
Full work available at URL: https://zenodo.org/record/1475065
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (1)
Uses Software
Cites Work
- Four decades of {\textsc{Mizar}}. Foreword
- MizAR 40 for Mizar 40
- Improving legibility of formal proofs based on the close reference principle is NP-hard
- The seventeen provers of the world. Foreword by Dana S. Scott..
- ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
- Set theory for verification. I: From foundations to functions
- On rewriting rules in Mizar
- Enhancement of Mizar Texts with Transitivity Property of Predicates
- The Twelf Proof Assistant
- Type Inference for ZFH
- Mizar: State-of-the-art and Beyond
- The Isabelle Framework
- On the Structure of Mizar Types
- Licensing the Mizar Mathematical Library
- A logical framework combining model and proof theory
This page was built for publication: Presentation and manipulation of Mizar properties in an Isabelle object logic
