Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar

DOI10.1007/978-3-642-14128-7_12zbMath1286.68403arXiv1005.4592OpenAlexW3100298706MaRDI QIDQ3582702

Josef Urban, Geoff Sutcliffe

Publication date: 24 August 2010

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

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

Mathematics Subject Classification ID

Knowledge representation (68T30)

Related Items (7)

Computer Certification of Generalized Rough Sets Based on Relations ⋮ The Mizar Mathematical Library in OMDoc: translation and applications ⋮ Formalizing Lattice-Theoretical Aspects of Rough and Fuzzy Sets ⋮ HOL(y)Hammer: online ATP service for HOL Light ⋮ Large Formal Wikis: Issues and Solutions ⋮ Initial Comparison of Formal Approaches to Fuzzy and Rough Sets ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)

Uses Software

• Unnamed Item
• Unnamed Item
• TPTP
• Metis_
• Mizar
• E Theorem Prover
• MaLARea
• SystemOnTPTP

This page was built for publication: Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar