Redukcja binarnych tablic decyzyjnych z wykorzystaniem automatycznego wnioskowania

• Autorzy: Adamski M. , Tkacz J. , Wrzesińska B.
• Języki publikacji: PL

Abstrakty

PL

W artykule przedstawiono sposób redukcji binarnych tablic decyzyjnych z wykorzystaniem systemu komputerowego dowodzenia twierdzeń w zdaniowym rachunku Gentzena [1, 4]. Binarna tablica decyzyjna przedstawia słabo określoną funkcję logiczną wielu zmiennych [6, 7]. Przykładową tablicę zaczerpnięto z książki [5], ze względu na zamieszczony w niej pełny i systematyczny opis wszystkich kroków minimalizacji funkcji i stopniowo uzyskiwanych rezultatów częściowych. Proponowany sposób minimalizacji symbolicznej postaci funkcji logicznej umożliwia w stosunkowo sprawny sposób otrzymywanie rezultatów dokładnych, wraz z formalnym dowodem ich gwarantowanej poprawności.

EN

The paper presents a new methodology for symbolic reduction of binary decision tables, currently intensively used for compact behavioral specifications of logic controllers. As an example the well known problem of simplification of a set of boolean relations with many variables and large sets of don’t care condition is chosen. They described also a special class of Boolean function called weakly specified or strongly unspecified. As a completely new, original solution, the formal automated reasoning based on Gentzen propositional calculus together with hypergraph theory are jointly used. The clique-transversal symbolic calculation is performed by means of effective reasoning in Gentzen calculus, giving the formal proof of all transformations.

Słowa kluczowe

PL

decyzyjne tablice binarne; hipergraf; poprzeczny; Gentzen; rozumowanie automatyczne

EN

binary decision tables; hypergraph; transversal; Gentzen; automated reasoning

• Wydawca: Komisja Informatyki Polskiej Akademii Nauk, Oddział w Gdańsku
• Czasopismo: Metody Informatyki Stosowanej
• Rocznik: 2010
• Tom: nr 3 (24)
• Strony: 5--12
• Opis fizyczny: Bibliogr. 11poz., tab.

Twórcy

autor

Adamski M.

autor

Tkacz J.

autor

Wrzesińska B.

• Uniwersytet Zielonogórski, Wydział Elektrotechniki, Informatyki i Telekomunikacji

Bibliografia

• [1] Adamski M., Projektowanie układów cyfrowych systematyczną metodą strukturalną. Monografie Nr 49. Wydawnictwo Wyższej Szkoły Inżynierskiej w Zielonej Górze, 1990, ISSN 0239-7390
• [2] Atserias, A., Galesi, N., and Pudlák, P. 2002. Monotone simulations of non-monotone proofs. J. Comput. Syst. Sci. 65, 4 (Dec. 2002), 626-638.
• [3] Eiter, T., Gottlob, G., and Makino, K. 2002. New results on monotone dualization and generating hypergraph transversals. Proc. of the 32th ACM Symp. STOC '02, 14-22.
• [4] Gallier J.H., Logic for computer science, Foundations of Automatic Theorem Proving. Harper & Row, (1986).
• [5] Gurtowcew L, Petrenko A.F., Czapenko W.P., Logiczeskoje projektirowanie ustrojstw awtomatiki. Izdatielstwo Zinatie, Riga 1978.
• [6] Łuba T., Synteza układów logicznych, Wyższa Szkoła Informatyki Stosowanej i Zarządzania, Warszawa, 2000.
• [7] Misiurewicz P., Perkowski M. Teoria automatów. Wydawnictwa Politechniki Warszawskiej, 1973
• [8] Sapiecha P., Algorytmy syntezy funkcji relacji boolowskich w aspekcie metod reprezentacji kompresji danych. Rozprawa doktorska. Politechnika Warszawska, Wydział Elektroniki i Technik Informacyjnych, Warszawa, 1998.
• [9] Sapiecha P., Pleban M., Łuba T, Zbierzchowski Dekompozycja funkcji i relacji boolowskich w syntezie logicznej i analizie danych. Kwartalnik Elektroniki i Telekomunikacji, 2000 Vol.46 (No.3)
• [10] Tkacz J., Adamski M., Projektowanie sekwencyjnych układów cyfrowych z wykorzystaniem logiki sekwentów Gentzena, Przegląd Elektrotechniczny, 2009, nr 7, s. 196-199.
• [11] Tkacz J., Projektowanie układów sterowania binarnego wspomagane automatycznym wnioskowaniem Gentzena, Rozprawa doktorska. Uniwersytet Zielonogórski, Wydział Elektrotechniki, Informatyki i Telekomunikacji, Zielona Góra, 2008.