Presenting and explaining Mizar

DOI10.1016/J.ENTCS.2006.09.022MaRDI QIDQ2867936zbMATH OpenOpenAlexFDO

Authors Josef Urban, Grzegorz Bancerek

Publication date 20 December 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2006.09.022

zbMATH Keywords

ATPMizarMML queryMPTPproof objectsproof presentation

Mathematics Subject Classification ID

Knowledge representation (68T30)

Recommendations

• ATP and presentation service for Mizar formalizations
• Mizar: state-of-the-art and beyond
• A comparison of Mizar and Isar
• Mathematical Knowledge Management
• MPTP 0.2: Design, implementation, and initial experiments

Cites work

• A Brief History of Natural Deduction
• Combining superposition, sorts and splitting
• scientific article; zbMATH DE number 1809861 (Why is no real title available?)
• scientific article; zbMATH DE number 1809862 (Why is no real title available?)
• scientific article; zbMATH DE number 1951634 (Why is no real title available?)
• scientific article; zbMATH DE number 2090305 (Why is no real title available?)
• Mathematical Knowledge Management
• Mathematical Knowledge Management
• Mathematical Knowledge Management
• Mathematical knowledge management. Third international conference, MKM 2004, Białowieża, Poland, September 19--21, 2004. Proceedings.
• MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics
• MPTP 0.2: Design, implementation, and initial experiments
• MPTP-motivation, implementation, first experiments
• On equivalents of well-foundedness. An experiment in MIZAR
• The TPTP problem library. CNF release v1. 2. 1

Cited in

(14)

• System description: XSL-based translator of Mizar to {\LaTeX}
• A comparison of Mizar and Isar
• Semantics of Mizar as an Isabelle object logic
• Presentation and manipulation of Mizar properties in an Isabelle object logic
• scientific article; zbMATH DE number 5850143 (Why is no real title available?)
• Mizar’s Soft Type System
• Automated reasoning and presentation support for formalizing mathematics in MizAR
• Towards Formal Proof Script Refactoring
• Mathematical Knowledge Management
• SAT-enhanced Mizar proof checking
• Mechanizing Mathematical Reasoning
• Mathematical Knowledge Management
• Mathematical Knowledge Management
• VizAR: visualization of automated reasoning proofs (system description)

Describes a project that uses

Uses Software

• MizarMode
• MPTP
• MPTP 0.2
• OTTER
• VAMPIRE
• SPASS
• TPTP
• MoMM
• Mizar
• MML
• E Theorem Prover

This page was built for publication: Presenting and explaining Mizar

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