Koncepcja i realizacja systemu wnioskującego Gentzena z wykorzystaniem RDBMS – IBM DB2

• Autorzy: Gaczyński A. , Tkacz J. , Doligalski M.

Warianty tytułu

EN

Concept and design of Gentzen deduction system in RDBMS - IBM DB2

• Języki publikacji: PL

Abstrakty

PL

Poniższy artykuł przedstawia realizację systemu wnioskującego Gentzena z wykorzystaniem systemu zarządzania relacyjną bazą danych IBM DB2 w wersji 9.7. Niniejsza publikacja prezentuje zalety z używania procedur składowanych oraz w jaki sposób można wykorzystać strukturę tabel w bazie danych do zaawansowanego przetwarzania informacji. Przedstawia użycie bazy danych przy implementacji automatycznych systemów dowodzenia twierdzeń oraz w jaki sposób architektura klient-serwer znajduje zastosowanie w stosunku do tego typu aplikacji.

EN

The paper presents conception and design of Gentzen deduction system by using RDBMS – IBM DB2. It shows adds of stored procedures and method of using table structure in database for advanced information computing. Testing of the solution is based on the analysis of randomly generated not oriented graphs. The tests confirm the correctness of implementations, and also highlight the problem of high computational complexity. This unusual implementation and use of RDBMS environment opens up new areas of research on the optimization of reasoning algorithm.

Słowa kluczowe

PL

wnioskowanie symboliczne; rachunek zdań; bazy danych; dowodzenie twierdzeń; theorem proving

EN

symbolic reasoning; databases

• Wydawca: Wydawnictwo SIGMA-NOT
• Czasopismo: Przegląd Elektrotechniczny
• Rocznik: 2012
• Tom: R. 88, nr 8
• Strony: 148--151
• Opis fizyczny: Bibliogr. 12 poz., rys., tab., wykr.

Twórcy

autor

Gaczyński A.

autor

Tkacz J.

autor

Doligalski M.

• Uniwersytet Zielonogórski, Instytut Informatyki i Elektroniki,

Bibliografia

• [1] Ben-Ari M.: Logika matematyczna w informatyce, Wydawnictwo Naukowo Techniczne, Warszawa 2005.
• [2] Indrzejczak A.: Wprowadzenie do rachunku sekwentów – zagadnienia metodologiczne, zastosowania. E-book. http://www.filozof.uni.lodz.pl/prac/ai/Gentzen.pdf
• [3] Gallier J. H.: Logic of Computer Science. Foundation of Automatic Theorem Proving. Hapv&Row Publisher, New York (1986)
• [4] Gentzen G.: Badania nad wnioskowaniem logicznym. Tłumaczenie z języka niemieckiego dr Kazimierz Trzęsicki. Sekcja Wydawnicza Filii UW w Białymstoku, Białystok, (1980)
• [5] Pawlak Z.: Automatyczne dowodzenie twierdzeń, Państwowe Zakłady Wydawnictw Szkolnych, Warszawa (1965)
• [6] Adamski M.: Projektowanie układów cyfrowych systematyczną metodą strukturalną, Wydawnictwo Wyższej Szkoły Inżynierskiej w Zielonej Górze, Zielona Góra, (1990)
• [7] Szajna J., Projektowanie układów cyfrowych z wykorzystaniem programowania logicznego. Wydawnictwo Politechniki Zielonogórskiej, (1996)
• [8] Tkacz J.: Projektowanie układów sterowania binarnego wspomagane automatycznym wnioskowaniem Gentzena, rozprawa doktorska, Uniwersytet Zielonogórski, Wydział Elektrotechniki, Informatyki i Telekomunikacji, (2008)
• [9] Tkacz J., Adamski M., Wykorzystanie komputerowego wnioskowania w projektowaniu kombinacyjnych układów sterowania, Przegląd Telekomunikacyjny, (2008), nr.6, 728- 730.
• [10] Thelen B.: Investigation of Algorithms for Computer-Aided Logic Design of Digital Circuits. PhD thesis, Universität Karlsruche, (1988)
• [11] Mathony H.J.: Uniwersal logic design algorithm and its application the synthesis of two-lewel switching circuits, IEE Proceedings Letters, Elsevier Science Publishers (North Holland), (1990), Vol.29, pp.195-210
• [12] SDJ Extra DB2 9.7, nr 35