Cargando…
Enhancement of properties in Mizar
A “property” in the Mizar proof-assistant is a construction that can be used to register chosen features of predicates (e.g., “reflexivity”, “symmetry”), operations (e.g., “involutiveness”, “commutativity”) and types (e.g., “sethoodness”) declared at the definition stage. The current implementation...
Autor principal: | |
---|---|
Formato: | Online Artículo Texto |
Lenguaje: | English |
Publicado: |
PeerJ Inc.
2020
|
Materias: | |
Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7924646/ https://www.ncbi.nlm.nih.gov/pubmed/33816970 http://dx.doi.org/10.7717/peerj-cs.320 |
_version_ | 1783659133129457664 |
---|---|
author | Korniłowicz, Artur |
author_facet | Korniłowicz, Artur |
author_sort | Korniłowicz, Artur |
collection | PubMed |
description | A “property” in the Mizar proof-assistant is a construction that can be used to register chosen features of predicates (e.g., “reflexivity”, “symmetry”), operations (e.g., “involutiveness”, “commutativity”) and types (e.g., “sethoodness”) declared at the definition stage. The current implementation of Mizar allows using properties for notions with a specific number of visible arguments (e.g., reflexivity for a predicate with two visible arguments and involutiveness for an operation with just one visible argument). In this paper we investigate a more general approach to overcome these limitations. We propose an extension of the Mizar language and a corresponding enhancement of the Mizar proof-checker which allow declaring properties of notions of arbitrary arity with respect to explicitly indicated arguments. Moreover, we introduce a new property—the “fixedpoint-free” property of unary operations—meaning that the result of applying the operation to its argument always differs from the argument. Results of tests conducted on the Mizar Mathematical Library are presented. |
format | Online Article Text |
id | pubmed-7924646 |
institution | National Center for Biotechnology Information |
language | English |
publishDate | 2020 |
publisher | PeerJ Inc. |
record_format | MEDLINE/PubMed |
spelling | pubmed-79246462021-04-02 Enhancement of properties in Mizar Korniłowicz, Artur PeerJ Comput Sci Digital Libraries A “property” in the Mizar proof-assistant is a construction that can be used to register chosen features of predicates (e.g., “reflexivity”, “symmetry”), operations (e.g., “involutiveness”, “commutativity”) and types (e.g., “sethoodness”) declared at the definition stage. The current implementation of Mizar allows using properties for notions with a specific number of visible arguments (e.g., reflexivity for a predicate with two visible arguments and involutiveness for an operation with just one visible argument). In this paper we investigate a more general approach to overcome these limitations. We propose an extension of the Mizar language and a corresponding enhancement of the Mizar proof-checker which allow declaring properties of notions of arbitrary arity with respect to explicitly indicated arguments. Moreover, we introduce a new property—the “fixedpoint-free” property of unary operations—meaning that the result of applying the operation to its argument always differs from the argument. Results of tests conducted on the Mizar Mathematical Library are presented. PeerJ Inc. 2020-11-30 /pmc/articles/PMC7924646/ /pubmed/33816970 http://dx.doi.org/10.7717/peerj-cs.320 Text en ©2020 Korniłowicz https://creativecommons.org/licenses/by/4.0/ This is an open access article distributed under the terms of the Creative Commons Attribution License (https://creativecommons.org/licenses/by/4.0/) , which permits unrestricted use, distribution, reproduction and adaptation in any medium and for any purpose provided that it is properly attributed. For attribution, the original author(s), title, publication source (PeerJ Computer Science) and either DOI or URL of the article must be cited. |
spellingShingle | Digital Libraries Korniłowicz, Artur Enhancement of properties in Mizar |
title | Enhancement of properties in Mizar |
title_full | Enhancement of properties in Mizar |
title_fullStr | Enhancement of properties in Mizar |
title_full_unstemmed | Enhancement of properties in Mizar |
title_short | Enhancement of properties in Mizar |
title_sort | enhancement of properties in mizar |
topic | Digital Libraries |
url | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7924646/ https://www.ncbi.nlm.nih.gov/pubmed/33816970 http://dx.doi.org/10.7717/peerj-cs.320 |
work_keys_str_mv | AT korniłowiczartur enhancementofpropertiesinmizar |