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 (WInf) Formalized Mathematics, 2014, Volume 22, Issue 1 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
forma-2014-0001.pdf | 263,17 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL