Semantics of Mizar as an Isabelle object logic
From MaRDI portal
Publication:2323445
DOI10.1007/s10817-018-9479-zzbMath1468.68290OpenAlexW2889093133WikidataQ108482110 ScholiaQ108482110MaRDI QIDQ2323445
Publication date: 2 September 2019
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-018-9479-z
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (6)
A new export of the Mizar mathematical library ⋮ Isabelle/HOL/GST: a formal proof environment for generalized set theories ⋮ Combining higher-order logic with set theory formalizations ⋮ Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. ⋮ Declarative Proof Translation (Short Paper) ⋮ Experiences from exporting major proof assistant libraries
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Four decades of {\textsc{Mizar}}. Foreword
- MizAR 40 for Mizar 40
- Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver
- A learning-based fact selector for Isabelle/HOL
- Topological manifolds
- MPTP-motivation, implementation, first experiments
- Mathematical knowledge management. Third international conference, MKM 2004, Białowieża, Poland, September 19--21, 2004. Proceedings.
- ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
- MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics
- MPTP 0.2: Design, implementation, and initial experiments
- Obvious inferences
- Set theory for verification. I: From foundations to functions
- The role of the Mizar mathematical library for interactive proof development in Mizar
- Flexary connectives in Mizar
- On the rules of suppositions in formal logic
- A compendium of continuous lattices in MIZAR
- A comparison of Mizar and Isar
- ATP and presentation service for Mizar formalizations
- The Mizar Mathematical Library in OMDoc: translation and applications
- Premise selection for mathematics by corpus analysis and kernel methods
- Presentation and manipulation of Mizar properties in an Isabelle object logic
- Accessing the Mizar Library with a Weakly Strict Mizar Parser
- Extracting Higher-Order Goals from the Mizar Mathematical Library
- Presenting and Explaining Mizar
- Asynchronous User Interaction and Tool Integration in Isabelle/PIDE
- A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving
- Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface
- A Consistent Foundation for Isabelle/HOL
- A Brief Overview of Mizar
- The Twelf Proof Assistant
- Type Inference for ZFH
- Mizar: State-of-the-art and Beyond
- The Lean Theorem Prover (System Description)
- A Declarative Language for the Coq Proof Assistant
- Partizan Games in Isabelle/HOLZF
- The Isabelle Framework
- Merging Procedural and Declarative Proof
- On a Practical Way of Describing Formal Deductions
- Isabelle Formalization of Set Theoretic Structures and Set Comprehensions
- Proof Auditing Formalised Mathematics
- Mathematical Knowledge Management
- Mathematical Knowledge Management
- A logical framework combining model and proof theory
- Alternative Aggregates in Mizar
- Random-Access Stored-Program Machines, an Approach to Programming Languages
- Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
- A Mechanized Translation from Higher-Order Logic to Set Theory
- Evaluation of Automated Theorem Proving on the Mizar Mathematical Library
- Mathematical Knowledge Management
- Formalization of the fundamental group in untyped set theory using auto2
This page was built for publication: Semantics of Mizar as an Isabelle object logic
