Back to Search
Start Over
Encoding transition systems in sequent calculus
- Source :
- Theoretical Computer Science. 294(3):411-437
- Publication Year :
- 2003
- Publisher :
- Elsevier BV, 2003.
-
Abstract
- 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 calculus.
- Subjects :
- Discrete mathematics
Geometry of interaction
Natural deduction
General Computer Science
Cut-elimination theorem
Noncommutative logic
Logic specification
Linear logic
Definitions
Curry–Howard correspondence
Transition systems
Theoretical Computer Science
Algebra
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
Proof calculus
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
Computer Science::Logic in Computer Science
Bisimulation
Sequent
Mathematics
Computer Science(all)
Subjects
Details
- ISSN :
- 03043975
- Volume :
- 294
- Issue :
- 3
- Database :
- OpenAIRE
- Journal :
- Theoretical Computer Science
- Accession number :
- edsair.doi.dedup.....10445f68c1b98d5e87f657dcf6721a4b
- Full Text :
- https://doi.org/10.1016/s0304-3975(01)00168-2