This paper develops a cyclic labelled proof-theoretic framework for process logic -- an extension of dynamic logic in which formulas specify properties of execution traces rather than only final states. The main difficulty is that first-order process logic must reason about concrete computations while preserving temporal information along regular-program traces. Existing compositional calculi cover important fragments, but do not provide a complete treatment of full first-order process logic over regular programs. We address this difficulty by enriching process-logic formulas with labels that explicitly record trace and update information during derivations. Based on this construction, we define cyclic labelled proof systems for propositional and first-order process logic, respectively denoted by G3PPL and G3FOPL. We prove the soundness by using the cyclic conditions to obtain an infinite descent in a well-founded multiset ordering, and prove the completeness by showing that the labelled systems can derive the established proof rules of process logic and first-order dynamic logic. The result is a uniform framework for process logic in which for the first time, trace-based program properties and first-order computations can be handled within the same proof structure.

翻译：本文为过程逻辑发展了一个循环带标签的证明论框架——过程逻辑是动态逻辑的扩展，其公式不仅描述最终状态，还描述执行轨迹的性质。主要难点在于一阶过程逻辑需在保持正则程序轨迹时间信息的同时对具体计算进行推理。现有组合演算虽覆盖重要片段，但未能完整处理正则程序上的全一阶过程逻辑。我们通过在过程逻辑公式中引入显式记录推导过程中轨迹与更新信息的标签来解决这一难点。基于此构造，我们分别为命题过程逻辑和一阶过程逻辑定义了循环带标签证明系统，记为G3PPL与G3FOPL。利用循环条件在良基多重序上获得无穷递降来证明可靠性，并通过证明带标签系统可推导出过程逻辑与一阶动态逻辑的已有证明规则来验证完备性。最终得到一个统一的过程逻辑框架，其中基于轨迹的程序性质与一阶计算首次可在同一证明结构内处理。