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 25
- Downloads 0
Analysis of inter-channel dependencies in audio lossless block coding
In this paper the basics of data predictive modeling (using the method of minimization mean square error) for lossless audio compression are presented. The described research focuses on inter-channel analysis and setting...
A Model-Driven Approach to Microservice Software Architecture Establishment
In this positional paper we propose a model-driven approach which addresses challenges related to modeling, development and deployment of software applications that follow the microservice architecture (MSA) design princ...
An Efficient Load Balancing Algorithms in Stream Processing With the Cloud Computing Environment
Fog personal computers is definitely correctly buzzword that is receiving, it provides firms zīmju base might be coming availability specialist knowledge. Impair price serve should you have of superiorities in studying t...
The Practical Use of Problem Encoding Allowing Cheap Fitness Computation of Mutated Individuals
The usual assumption in the Evolutionary Computation field is that a cost of computing single fitness function evaluation is at last similar for all cases. Such assumption does not have to be true. In this paper we consi...
Importance of Text Data Preprocessing & Implementation in RapidMiner
Data preparation is an important phase before applying any machine learning algorithms. Same with the text data before applying any machine learning algorithm on text data, it requires data preparation. The data preparat...