Encoding transition systems in sequent calculus

DOI10.1016/S0304-3975(01)00168-2zbMATH Open1028.68095MaRDI QIDQ1398474FDOQ1398474

Authors: Raymond McDowell, Catuscia Palamidessi, Dale Miller 

Publication date: 29 July 2003

Published in: Theoretical Computer Science (Search for Journal in Brave)

Recommendations

• scientific article; zbMATH DE number 1231524
• scientific article; zbMATH DE number 2152687
• scientific article; zbMATH DE number 1950250
• A hybrid linear logic for constrained transition systems
• A formal framework for specifying sequent calculus proof systems

zbMATH Keywords

Linear logicBisimulationDefinitionsLogic specificationTransition systems

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Linear logic
• A calculus of communicating systems
• Logic programming and negation: A survey
• Partial inductive definitions
• Title not available (Why is that?)
• Title not available (Why is that?)
• Cut-elimination for a logic with definitions and induction
• Forum: A multiple-conclusion specification logic
• Contributions to the Theory of Logic Programming
• A unification algorithm for typed \(\overline\lambda\)-calculus
• A Proof-Theoretic Approach to Logic Programming
• Title not available (Why is that?)
• From operational semantics to abstract machines
• A Complete Axiomatization of the Three valued Completion of Logic Programs

Cited In (17)

• Logic of transition systems
• Macrotransducers and applicative systems for partially continuous functions
• Attributed transition systems with hidden transitions
• A hybrid linear logic for constrained transition systems
• Relating reasoning methodologies in linear logic and process algebra
• Nominal abstraction
• Automatic verification of secrecy properties for linear logic specifications of cryptographic protocols
• Relating state-based and process-based concurrency through linear logic (full-version)
• Cut elimination for a logic with induction and co-induction
• Encoding generic judgments: preliminary results
• Title not available (Why is that?)
• A proof theory for model checking
• Constructing weak simulations from linear implications for processes with private names
• Relating state-based and process-based concurrency through linear logic
• Modal transition system encoding of featured transition systems
• Extracting proofs from tabled proof search
• Title not available (Why is that?)

Uses Software

• ML

This page was built for publication: Encoding transition systems in sequent calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1398474)