Dane o rozprawie doktorskiej

Rodzaj pracy	Rozprawa doktorska
Data uzyskania stopnia	2008-12-12
Uzyskany stopień naukowy	Doktor nauk technicznych
Promotor	Prof. dr hab. inż. Marian Adamski, Uniwersytet Zielonogórski, Instytut Informatyki i Elektroniki
Recenzenci	Prof. dr hab. inż. Aleksander Barkalov, Uniwersytet Zielonogórski, Instytut Informatyki i Elektroniki prof. dr hab. inż. Tadeusz Łuba, Politechnika Warszawska, Instytut Telekomunikacji
Jednostka prowadząca przewód	Uniwersytet Zielonogórski, Wydział Elektrotechniki Informatyki i Telekomunikacji
Miejsce pracy autora rozprawy	Uniwersytet Zielonogórski, Wydział Elektrotechniki Informatyki i Telekomunikacji, Instytut Informatyki i Elektroniki
Dziedzina naukowa	Nauki techniczne
Dyscyplina naukowa	Informatyka
Specjalność naukowa	Technika cyfrowa
Sposób zgłoszenia rozprawy, dostępność, liczba stron	Nie ogłoszono, Biblioteka Główna Uniwersytetu Zielonogórskiego, s. 130
Wydawca
Słowa kluczowe	Sekwent, wnioskowanie symboliczne, Gentzen, logika matematyczna, technika cyfrowa, drzewo dowodu

Streszczenie

W rozprawie doktorskiej zaproponowano nową koncepcję systemu wnioskowania symbolicznego Gentzena oraz przedstawiono jego techniczną realizację. Omówiono szereg usprawnień algorytmu zwiększających jego efektywność, szczególnie przy normalizacji dużej liczby wyrażeń logicznych. Nowatorski system CAD może transformować złożone opisy funkcjonowania układów cyfrowych przedstawione w sposób behawioralny do prostej postaci, które mogą być mapowane bezpośrednio w strukturach FPGA. Poprzez zastosowanie transformacji znormalizowanego opisu do formatu ESPRESSO umożliwiono współpracę systemu wnioskującego z systemami uniwersyteckimi takimi jak VIS, SIS, czy DEMAIN. Współpraca z systemami komercyjnymi umożliwiona została poprzez transformację wyrażeń znormalizowanych na języki opisu sprzętu (VHDL i Verilog).
W rozprawie proponuje się wspomaganie wnioskowaniem sterowania binarnego (np. synteza, analiza, testowanie i weryfikacja). Uniwersalności algorytmu wnioskowania umożliwiła zastosowanie go również do rozwiązywania problemów naukowych, takich jak analiza kombinatoryczna grafów, czy rozwiązywanie zawiłych problemów logicznych.

Własności opracowanego algorytmu oraz jego uniwersalność mogą spowodować szerokie zainteresowanie oraz przydatność w przyszłych badaniach naukowych, niekoniecznie związanych bezpośrednio z techniką cyfrową.

Abstact

There are presented a new idea of an application of Gentzen logic symbolic reasoning for solving some combinational problems in the digital system design in this Ph.D. Thesis. Although there are described a particular kind of logic algorithms optimization and some possibilities of increasing efficiency of the presented application for the normalizing a great number of symbolic expressions. The new CAD system is able to transform very complicated behavioral descriptions into simple expressions, which can be directly mapped into FPGA structures. On the other hand the system produces an ESPRESSO format, which makes possibility of easy cooperate with popular university systems like VIS, SIS or DEMAIN. Proposed system could also cooperate with known commercial CAD systems by making transformation from normalized digital system description into HDL languages like VHDL and Verilog.
The aid of the design process of logic circuits is applied in different stages of this process like synthesis, analysis, decomposition or testing and verification. Additionally, because this algorithm has universal form, it can be also used for resolving scientific problems like combinatorial graph analysis or resolving of difficult logical problems.

All these aspects makes that proposed algorithm could have wide range of applications and it could be also a very interesting background for further scientific researches.