PL EN


Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
Tytuł artykułu

Redukcja binarnych tablic decyzyjnych z wykorzystaniem automatycznego wnioskowania

Identyfikatory
Warianty tytułu
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.
Rocznik
Tom
Strony
5--12
Opis fizyczny
Bibliogr. 11poz., tab.
Twórcy
autor
autor
  • 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.
Typ dokumentu
Bibliografia
Identyfikator YADDA
bwmeta1.element.baztech-article-BPS3-0018-0001
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ć.