Advancements in Logic and Process Algebra: Refinement and Unification

The recent publications in the field of logic and process algebra demonstrate a strong trend towards the refinement and unification of theoretical frameworks. A significant focus is on enhancing the precision and applicability of bisimilarity concepts in systems with time constraints, aiming to provide more robust foundations for analyzing and verifying concurrent processes. Additionally, there is a notable effort in advancing syntactic methods for cut-elimination in provability logic, with a particular emphasis on simplifying and clarifying existing procedures. This is complemented by the development of unified Gentzen-style frameworks for various temporal and connexive logics, which not only streamline the proof systems but also establish important theoretical results such as cut-elimination and normalization theorems. These developments collectively push the boundaries of formal logic and process algebra, offering more powerful tools for theoretical exploration and practical application.

Noteworthy Papers

  • Concrete Branching Bisimilarity for Processes with Time-outs: Introduces a precise adaptation of branching bisimilarity for systems with time-outs, complete with a modal characterisation and congruence proof.
  • Syntactic Cut-Elimination for Provability Logic GL via Nested Sequents: Offers a clearer and more straightforward approach to cut-elimination in provability logic, reducing ambiguity and complexity.
  • A Unified Gentzen-style Framework for Until-free LTL: Presents a comprehensive framework for until-free linear-time temporal logic, unifying sequent calculus and natural deduction systems.
  • Unified Gentzen Approach to Connexive Logics over Wansing's C: Develops Gentzen-style systems for a family of connexive logics, demonstrating equivalence and establishing cut-elimination and normalization theorems.

Sources

Concrete Branching Bisimilarity for Processes with Time-outs

Syntactic Cut-Elimination for Provability Logic GL via Nested Sequents

A Unified Gentzen-style Framework for Until-free LTL

Unified Gentzen Approach to Connexive Logics over Wansing's C

Built with on top of