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...

Descripción completa

Detalles Bibliográficos
Autor principal: Korniłowicz, Artur
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