Wyniki wyszukiwania - BazTech

Ograniczanie wyników

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: Gentzen sequents

Sortuj według:

Ogranicz wyniki do:

Structured Mapping of Petri Net States and Events for FPGA Implementations

Tkacz J., Adamski M.

International Journal of Electronics and Telecommunications

2013

Vol. 59, No. 4

331-339

The paper presents a new method of structured encoding of global internal states and events in Reconfigurable Logic Controllers, which are directly mapped into Field Programmable Gate Arrays (FPGA). Modular, concurrently decomposed, colored state machine is chosen as a intermediate model, before the mapping of Petri net into an array structure of dedicated but very flexible and reliable digital system. The initial textual specification in formal Gentzen logic serves both as a design description for a rapid prototyping, as well as formal model, suitable for detailed computer-based reasoning about optimized and synthesized logic controller, implemented in configurable hardware. Only the selected linear subset from general, universal propositional Gentzen Logic is necessary to deduce several properties of the net, such as relations of nonconcurrency among structurally ordered macroplaces. The goal of this paper is to present the design methodology for modeling and synthesis of discrete controllers using related Petri net theory, rule-based theory (mathematical logic), and VHDL.

A Survay of Foundational Gentzen's Systems for Finitely-Valued Logics

Borowik P.

Scientific Issues of Jan Długosz University in Częstochowa. Mathematics

1998

Vol. 4

89-120

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.