Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
Tytuł: Concatenation of Finite Sequences
Autorzy: Ziobro, Rafał
Słowa kluczowe: finite sequence
finite 0-sequence
Data wydania: 2019
Data dodania: 21-maj-2019
Wydawca: DeGruyter Open
Źródło: Formalized Mathematics, Volume 27, Issue 1, Pages 1-13
Abstrakt: The coexistence of “classical” finite sequences [1] and their zero-based equivalents finite 0-sequences [6] in Mizar has been regarded as a disadvantage. However the suggested replacement of the former type with the latter [5] has not yet been implemented, despite of several advantages of this form, such as the identity of length and domain operators [4]. On the other hand the number of theorems formalized using finite sequence notation is much larger then of those based on finite 0-sequences, so such translation would require quite an effort. The paper addresses this problem with another solution, using the Mizar system [3], [2]. Instead of removing one notation it is possible to introduce operators which would concatenate sequences of various types, and in this way allow utilization of the whole range of formalized theorems. While the operation could replace existing FS2XFS, XFS2FS commands (by using empty sequences as initial elements) its universal notation (independent on sequences that are concatenated to the initial object) allows to “forget” about the type of sequences that are concatenated on further positions, and thus simplify the proofs.
Afiliacja: Department of Carbohydrate Technology, University of Agriculture, Krakow, Poland
DOI: 10.2478/forma-2019-0001
ISSN: 1426-2630
e-ISSN: 1898-9934
metadata.dc.identifier.orcid: 0000-0001-9681-4380
Typ Dokumentu: Article
Występuje w kolekcji(ach):Formalized Mathematics, 2019, Volume 27, Issue 1

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
forma_2019_27_1_001.pdf250,4 kBAdobe PDFOtwórz
Pokaż pełny widok rekordu Zobacz statystyki

Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL Creative Commons