The way from linearly written derivations in natural deduction, introduced by Jaskowski and often used in textbooks, is a straightforward root-first translation. The other direction, instead, is tricky, because of the partially ordered assumption formulas in a tree that can get closed by the end of a derivation. An algorithm is defined that operates alternatively from the leaves and root of a derivation and solves the problem.
W referacie przedstawiono koncepcję i sposób weryfikacji specyfikacji sterowników logicznych z wykorzystaniem wnioskowania Gentzena. Zastosowanie symbolicznej metody Gentzena w odróżnieniu od opisywanych w literaturze rozwiązań, pozwala na pominięcie szeregu kroków w procesie analizy symbolicznej sieci Petriego, opisującej funkcjonowanie sterownika, co prowadzi do pełnej automatyzacji procesu weryfikacji. Metoda dokładnie określa fragmenty specyfikacji, w których występują defekty (np. zastoje).
EN
The paper presents a concept and methodology for verification of logic control-lers specification by means of using Gentzen symbolic deduction. This method omits some steps of algorithm of Petri net symbolic analysis, where Petri net specifies behavior of logic controller. This concept makes possible to automate full process of verification and determines places, for which specification has errors (deadlocks).
3
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
W artykule przedstawiono nowatorski sposób analizy systemów regułowych z wykorzystaniem symbolicznego wnioskowania w monotonicznej logice sekwentów Gentzena. Badany system dyskretny jest opisywany w postaci tablicy decyzyjnej. Celem analizy systemu jest usunięcie zbytecznych kolumn w tablicy decyzyjnej oraz nieistotnych symboli zmiennych logicznych w jej poszczególnych wierszach. Efektywny aparat wnioskowania w logice formalnej umożliwia sprawne wyznaczanie transwersal krawędzi hipergrafu rozróżnialności.
EN
The paper presents a new methodology for symbolic reduction of multivalued 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 several logic rules with many variables is chosen. 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.
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ć.