Automated reasoning and presentation support for formalizing mathematics in MizAR

DOI10.1007/978-3-642-14128-7_12zbMATH Open1286.68403arXiv1005.4592OpenAlexW3100298706MaRDI QIDQ3582702FDOQ3582702

Authors: Josef Urban, Geoff Sutcliffe 

Publication date: 24 August 2010

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Abstract: This paper presents a combination of several automated reasoning and proof presentation tools with the Mizar system for formalization of mathematics. The combination forms an online service called MizAR, similar to the SystemOnTPTP service for first-order automated reasoning. The main differences to SystemOnTPTP are the use of the Mizar language that is oriented towards human mathematicians (rather than the pure first-order logic used in SystemOnTPTP), and setting the service in the context of the large Mizar Mathematical Library of previous theorems,definitions, and proofs (rather than the isolated problems that are solved in SystemOnTPTP). These differences poses new challenges and new opportunities for automated reasoning and for proof presentation tools. This paper describes the overall structure of MizAR, and presents the automated reasoning systems and proof presentation tools that are combined to make MizAR a useful mathematical service.

Full work available at URL: https://arxiv.org/abs/1005.4592

Recommendations

• ATP and presentation service for Mizar formalizations
• Custom automations in Mizar
• Presenting and explaining Mizar
• Mizar: state-of-the-art and beyond
• Mathematical knowledge management in MIZAR

Mathematics Subject Classification ID

Knowledge representation (68T30)

Cited In (11)

• Extracting Higher-Order Goals from the Mizar Mathematical Library
• Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization
• Automated Improving of Proof Legibility in the Mizar System
• Computer certification of generalized rough sets based on relations
• The Mizar Mathematical Library in OMDoc: translation and applications
• Large formal wikis: issues and solutions
• ATP and presentation service for Mizar formalizations
• HOL(y)Hammer: online ATP service for HOL Light
• Formalizing lattice-theoretical aspects of rough and fuzzy sets
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Initial comparison of formal approaches to fuzzy and rough sets

Uses Software

• MizarMode
• MPTP 0.2
• TPTP
• Metis_
• Mizar
• E Theorem Prover
• MaLARea
• SystemOnTPTP

This page was built for publication: Automated reasoning and presentation support for formalizing mathematics in MizAR

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