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 19
- Downloads 0
Modular Multi-Objective Deep Reinforcement Learning with Decision Values
In this work we present a method for using Deep Q-Networks (DQNs) in multi-objective environments. Deep Q-Networks provide remarkable performance in single objective problems learning from high-level visual state represe...
Detection of Arrhythmia using Neural Network
There is an increase in cardio logical patients all over the world due to change in modern life style. It forces the medical researchers to search for smart devices that can diagnosis and predict the onset of cardiac pro...
Detection of Malicious Executables Using Rule Based Classification Algorithms
Machine Learning class rule has varied packages together with classification, clustering, will understand association rules furthermore and is capable of the method an enormous set of the information set as measure super...
Kestrel-based Search Algorithm (KSA) and Long Short Term Memory (LSTM) Network for feature selection in classification of high-dimensional bioinformatics datasets
Although deep learning methods have been applied to the selection of features in the classification problem, current methods of learning parameters to be used in the classification approach can vary in accuracy at each t...
Application of ASIP in Embedded Design with Optimized Clock Management
As the demand for high performance computing increases, new approaches have to be found to automate the design of embedded processors. Simultaneously, new tools have to be developed to short the execution time consumptio...