Rule-based formal specification and implementation of logic controllers programs

The paper describes a proposed framework for the synthesis of structural, rule-based descriptions in Gentzen sequent logic language that could be derived from behavioural descriptions in interpreted Petri net (or control Petri net, Grafcet, sequential function chart, Grafchart formats). The interpreted Petri net is considered as a main, initial specification format for programmable logic controller programs. The Gentzen system allows one to naturally simulate and denote the human reasoning and clearly perform symbolic transformations. In such a way, it is possible to combine mathematical clarity with practical usefulness. The specification in the form of symbolic expressions may be transformed into a format accepted by standard tools (PLD compilers, VHDL, PLC programming languages) as well as into the standard Boolean expressions