REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: http://hdl.handle.net/11320/3697
Tytuł: Definition of Flat Poset and Existence Theorems for Recursive Call
Autorzy: Ishida, Kazuhisa
Shidama, Yasunari
Grabowski, Adam
Słowa kluczowe: flat posets
recursive calls for posets
flattening operator
Data wydania: 2014
Data dodania: 9-gru-2015
Wydawca: De Gruyter Open
Źródło: Formalized Mathematics, Volume 22, Issue 1, 2014, Pages 1-10
Abstrakt: This text includes the definition and basic notions of product of posets, chain-complete and flat posets, flattening operation, and the existence theorems of recursive call using the flattening operator. First part of the article, devoted to product and flat posets has a purely mathematical quality. Definition 3 allows to construct a flat poset from arbitrary non-empty set [12] in order to provide formal apparatus which eanbles to work with recursive calls within the Mizar langauge. To achieve this we extensively use technical Mizar functors like BaseFunc or RecFunc. The remaining part builds the background for information engineering approach for lists, namely recursive call for posets [21].We formalized some facts from Chapter 8 of this book as an introduction to the next two sections where we concentrate on binary product of posets rather than on a more general case.
Afiliacja: Ishida Kazuhisa - Neyagawa-shi Osaka, Japan
Shidama Yasunari - Shinshu University Nagano, Japan
Grabowski Adam - Institute of Informatics University of Białystok Akademicka 2, 15-267 Białystok Poland
URI: http://hdl.handle.net/11320/3697
DOI: 10.2478/forma-2014-0001
ISSN: 1426-2630
1898-9934
Typ Dokumentu: Article
Występuje w kolekcji(ach):Artykuły naukowe (WMiI)
Formalized Mathematics, 2014, Volume 22, Issue 1

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
forma-2014-0001.pdf263,17 kBAdobe PDFOtwórz
Pokaż pełny widok rekordu Zobacz statystyki


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