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.
Przedstawiono możliwości zastosowania komputerowego wnioskowania symbolicznego Gentzena w projektowaniu układów cyfrowych oraz do rozwiązywania skomplikowanych problemów logicznych. Wykorzystując przykład sterownika zaczerpnięty z literatury, przedstawiono sposób uzyskiwania uproszczonego opisu układu kombinacyjnego, kilkukrotnie odwołujący się do systemu wnioskującego. Metoda polega na zastąpieniu silnie nieokreślonej klasycznej tablicy decyzyjnej sekwentami, które opisują relacje pomiędzy wejściami i wyjściami układu. W wyniku normalizacji tych sekwentów otrzymuje się zbiór reguł typu if-then, równoważny formie koniunkcyjnej lub dysjunkcyjnej funkcji boolowskich.
EN
The paper presents a new idea of an application of Gentzen logic symbolic reasoning for solving some combinational problems in the digital system design. Taking into account an example of industrial combinational logic controller, which could be alternatively described in classic way as an binary decision table, it is demonstrated how to apply a new efficient version of automated theorem prover in propositional sequent logic for a direct design from behavioural specification.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.