MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics

DOI10.1016/j.jal.2005.10.004zbMath1107.68103OpenAlexW1972647229MaRDI QIDQ865631

Josef Urban

Publication date: 20 February 2007

Published in: Journal of Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jal.2005.10.004

zbMATH Keywords

MizarMizarModeproof assistance

Mathematics Subject Classification ID

Related Items (13)

A Programmer’s Text Editor for a Logical Theory: The SUMOjEdit Editor (System Description) ⋮ Mizar: State-of-the-art and Beyond ⋮ Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library ⋮ New Developments in Parsing Mizar ⋮ MPTP 0.2: Design, implementation, and initial experiments ⋮ ATP and presentation service for Mizar formalizations ⋮ Custom automations in Mizar ⋮ MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance ⋮ Pollack-inconsistency ⋮ MizarMode ⋮ Semantics of Mizar as an Isabelle object logic ⋮ Automated Improving of Proof Legibility in the Mizar System ⋮ Presenting and Explaining Mizar

Uses Software

• MPTP
• MoMM
• Mizar
• MML
• E Theorem Prover

Cites Work

• MPTP-motivation, implementation, first experiments
• On equivalents of well-foundedness. An experiment in MIZAR
• A Brief History of Natural Deduction
• Mathematical Knowledge Management
• Unnamed Item
• Unnamed Item

This page was built for publication: MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics