Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 4

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last
Wyniki wyszukiwania
Wyszukiwano:
w słowach kluczowych:  Gentzen logic
help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
PL
Artykuł jest ilustracją możliwości zastosowania komputerowego wnioskowania symbolicznego w projektowaniu układów cyfrowych, a w tym do rozwiązywania skomplikowanych problemów logicznych. Wykorzystując przykład sieci działań zaczerpnięty z literatury, przedstawiono sposób uzyskiwania uproszczonego opisu bloku kombinacyjnego automatu cyfrowego na podstawie jego specyfikacji regułowej. Metoda polega na zastąpieniu sekwentami tablicy przejść-wyjść automatu i przeprowadzeniu syntezy logicznej metodą komputerowego wnioskowania.
EN
There is presented a new idea of an application of Gentzen logic symbolic reasoning for solving some combinational problems in the sequential circuit design. Behavioral description of combinatorial block of synchronous control unit is given as flowchart. The method is realized by a replacement of the transition table by the sequents, which describe relations between inputs and outputs of combinatorial block of sequential digital circuit in rule based format.
PL
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.
PL
W referacie przedstawiono sposób dekompozycji sieci Petriego za pomocą naturalnego wnioskowania Gentzena na podsieci typu automatowego. Normalizacja i minimalizacja zbioru reguł z zastosowaniem algorytmu wnioskującego może zostać wykorzystana w procesach wyznaczania podsieci automatowych reprezentujących zdekomponowane, niezależne fragmenty większego układu sterowania. Prezentowana metoda, w odróżnieniu od innych, znanych z literatury, nie wymaga pełnego przekształcenia równania charakterystycznego, reprezentującego listę sąsiedztwa w celu uzyskania pierwszego rozwiązania.
EN
The paper presents a concept and design methodology for decomposition of logic controllers' specification by means of using Gentzen symbolic reasoning. Specification of logic controller behaviour can be represented by Petri net, which can be decomposed into simplified subnets. These subnets directly represent smaller and independent parts of logic controller. The first result (Petri net State Machine-subnet), obtained from symbolic deduction, can be generated without complete analysis of characteristic logic expression, created from local state space description.
4
Content available remote A Survay of Foundational Gentzen's Systems for Finitely-Valued Logics
EN
The Gentzen system for n-valued logical calculi discussed here is based on the notion of a sequent. However, this notion can be defined in at least three different ways. The first defines a sequent as a finite sequence of formulas (Kirin 1985, Saloni 1972, Orłowska 1985), the second defines it as an ordered n-tuple of finite sequences or sets of formulas (Rousseau 1967, Takahasi 1967, Borowik 1984). The third way consists in defining a sequent as an ordered pair of finite sets or sequences of formulas (Fitting 1991). The assumed definition determines then the form of the rules for eliminating or introducing propositional connectives in a given sequent, and thus also the whole formalization of the system.
first rewind previous Strona / 1 next fast forward last
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ć.