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 27
- Downloads 0
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 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...
A Non-Deterministic Strategy for Searching Optimal Number of Trees Hyperparameter in Random Forest
In this paper, we present a non-deterministic strategy for searching for optimal number of trees hyperparameter in Random Forest (RF). Hyperparameter tuning in Machine Learning (ML) algorithms is essential. It optimizes...
An Innovative B2C E-commerce Websites Selection using the ME-OWA and Fuzzy AHP
Today internet has emerged as a huge marketplace of products and services for meeting needs of more than a million customers worldwide. It provides users a platform to access information globally in electronic form as we...