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

DOI10.1016/J.JAL.2005.10.004zbMATH Open1107.68103OpenAlexW1972647229MaRDI QIDQ865631FDOQ865631

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

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• MPTP-motivation, implementation, first experiments
• On equivalents of well-foundedness. An experiment in MIZAR
• Mathematical Knowledge Management
• A Brief History of Natural Deduction

Cited In (16)

• Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library
• Presenting and explaining Mizar
• Mizar: State-of-the-art and Beyond
• Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization
• Automated Improving of Proof Legibility in the Mizar System
• mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library
• MizarMode
• ATP and presentation service for Mizar formalizations
• Custom automations in Mizar
• Pollack-inconsistency
• MPTP 0.2: Design, implementation, and initial experiments
• A Programmer’s Text Editor for a Logical Theory: The SUMOjEdit Editor (System Description)
• MikiBeta : A General GUI Library for Visualizing Proof Trees
• Semantics of Mizar as an Isabelle object logic
• New Developments in Parsing Mizar
• MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance

Uses Software

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

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

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