Mizar Set Comprehension in Isabelle Framework
Journal Title: Annals of Computer Science and Information Systems - Year 2018, Vol 17, Issue
Abstract
The Mizar project from its beginning aimed to make a highly human oriented proof environment where the proof style closely reflects the informal proofs style. The support is reflected in the size of the largest consistent formal library\mbox{\,---\,}Mizar Mathematical Library (MML). However, the Mizar system is the only tool that provides full verification and further development of the MML. In this paper, we present the progress in the development of the Isabelle/Mizar project whose main goal is independent cross-verification of the MML in Isabelle. We focus on Mizar set comprehension operators that allow defining sets that satisfy a given predicate. The development already covers simple cases where the arity of predicates is limited to two. We propose an infrastructure that provides a more elegant and recursive approach to construct and to provide the main property of set comprehension operators.
Authors and Affiliations
Karol Pąk
Keywords
Related Articles
- EP ID EP568232
- DOI 10.15439/2018F106
- Views 26
- Downloads 0
Inference rules for OWL-P in N3Logic
This paper presents OWL-P that is a lightweight formalism of OWL2. Before proposing our solution we have analyzed the OWL fragment that is actually used on the Web. OWL-P supports easy inferences by omitting complex lang...
Acoustic Model Training, using Kaldi, for Automatic Whispery Speech Recognition
The article presents research on the automatic whispery speech recognition. The main task was to find dependences between a number of triphone classes (number of leaves in decision tree) and the total number of Gaussian...
Assistive Smart, Structured 3D Environmental Information for the Visually Impaired and Blind: Leveraging the INSPEX Concept
Inspired by the abilities of contemporary autonomous vehicles to navigate with a high degree of effectiveness, the INSPEX Project 1 seeks to minaturise the sensing and processing technology involved, to produce devices w...
A Contemplating approach for Hive and Map reduce for efficient Big Data Implementation
In the reference current scenario, data is incremented exponentially and speed of data accruing at the rate of petabytes. Big data defines the available amount of data over the different media or wide communication media...
A Detailed Study of EEG based Brain Computer Interface
Brain Computer Interface (BCI) generate a direct method to communicate with the outside world. Many patients are not able to communicate. For example:- the patient who are suffered with the several disease like post stro...