Computer Science – Artificial Intelligence
Scientific paper
2010-05-25
Intelligent Computer Mathematics 2010, LNCS 6167, pp. 132-146
Computer Science
Artificial Intelligence
To appear in 10th International Conference on. Artificial Intelligence and Symbolic Computation AISC 2010
Scientific paper
10.1007/978-3-642-14128-7_12
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.
Sutcliffe Geoff
Urban Josef
No associations
LandOfFree
Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-298426