Automated reasoning and presentation support for formalizing mathematics in Mizar

Josef Urban, Geoff Sutcliffe

Research output: Chapter in Book/Report/Conference proceedingConference contribution

25 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationIntelligent Computer Mathematics - 10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010, Proceedings
Pages132-146
Number of pages15
DOIs
StatePublished - Jul 29 2010
Event10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010 - Paris, France
Duration: Jul 5 2010Jul 10 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6167 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010
CountryFrance
CityParis
Period7/5/107/10/10

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Automated reasoning and presentation support for formalizing mathematics in Mizar'. Together they form a unique fingerprint.

  • Cite this

    Urban, J., & Sutcliffe, G. (2010). Automated reasoning and presentation support for formalizing mathematics in Mizar. In Intelligent Computer Mathematics - 10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010, Proceedings (pp. 132-146). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6167 LNAI). https://doi.org/10.1007/978-3-642-14128-7_12