Presenting and Explaining Mizar

DOI10.1016/j.entcs.2006.09.022zbMath1278.68283OpenAlexW2049282215MaRDI QIDQ2867936

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

ATPMizarMPTPproof presentationproof objectsMML query

Mathematics Subject Classification ID

Knowledge representation (68T30)

Related Items (2)

Towards Formal Proof Script Refactoring ⋮ Semantics of Mizar as an Isabelle object logic

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• MPTP-motivation, implementation, first experiments
• 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
• The TPTP problem library. CNF release v1. 2. 1
• On equivalents of well-foundedness. An experiment in MIZAR
• A Brief History of Natural Deduction
• Mathematical Knowledge Management
• Mathematical Knowledge Management
• Mathematical Knowledge Management

This page was built for publication: Presenting and Explaining Mizar