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 22
- Downloads 0
An Adaptive Approach Digital Image Watermarking based on Discrete Wavelet Transform (DWT)
The applications of different dimension of multimedia have been grown rapidly on daily basis. Digital media brings about the changes in the conveniences to the people, The cons of this technology is security threat if th...
Static typing and dependency management for SOA
Several problems related to work reliability appear while building service-oriented systems. The first problem consists in lack of static typing and lack of inter-service data type checking. The second one consists in hi...
E-Assessment Tools for Programming Languages: A Review
Continuous Evaluation and feedback not only helps in improving learning of a student, but also acts as a constant motivator to put in more efforts. But then, feedback and assessment are very difficult and time consuming...
A Survey on Advanced Approaches of EHR in inter-related data using Machine Learning
Medical data is being used for huge number of research works over the globe which is for predicting something novel case studies in each work. The current research which we are handling is on utilizing the EHR (Electroni...
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...