Encoding Transition Systems in Sequent Calculus
Raymond McDowell, Dale Miller and Catuscia Palamidessi
Intuitionistic and linear logics can be used to specify
the operational semantics of transition systems in various ways.
We consider here two encodings: one uses linear logic and maps
states of the transition system into formulas,
and the other uses intuitionistic logic and maps states into terms.
In both cases, it is possible to relate transition paths
to proofs in sequent calculus.
In neither encoding, however, does it seem possible to capture
properties, such as simulation and bisimulation,
that need to consider all possible transitions or all
possible computation paths.
We consider augmenting both intuitionistic and linear logics with a
proof theoretical treatment of definitions.
In both cases, this addition allows proving various judgments concerning
simulation and bisimulation (especially for
noetherian transition systems).
We also explore the use of infinite proofs to reason about
infinite sequences of transitions.
Finally, combining definitions and induction into sequent calculus
proofs makes it possible to reason more richly about properties
of transition systems completely within the formal setting of sequent