Wyniki wyszukiwania - BazTech

Ograniczanie wyników

1 Metody Informatyki Stosowanej

1 2010

Powiadomienia systemowe

Sesja wygasła!

Znaleziono wyników: 1

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: poprzeczny

Sortuj według:

Ogranicz wyniki do:

Redukcja binarnych tablic decyzyjnych z wykorzystaniem automatycznego wnioskowania

Adamski M., Tkacz J., Wrzesińska B.

Metody Informatyki Stosowanej

2010

nr 3 (24)

5-12

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.

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.