收缩的唯一解、CCS及其HOL形式化
Unique Solutions of Contractions, CCS, and their HOL Formalisation
摘要：
收缩的唯一解是一种双相似性的证明技术，它克服了米尔纳的“方程的唯一解”技术的某些语法限制。本文概述了一个相当全面的形式化的核心理论CCS的HOL定理证明（HOL4），重点对理论的唯一解决方案的收缩。(The形式化由大约20，000行标准ML的证明脚本组成。理论本身的一些改进。特别是，我们删除的限制总和，这必须是弱保护，通过移动到根收缩，也就是说，包含在收缩预序的coarthorough precongruence。
英文摘要：
The unique solution of contractions is a proof technique for bisimilarity that overcomes certain syntactic constraints of Milner's "unique solution of equations" technique. The paper presents an overview of a rather comprehensive formalisation of the core of the theory of CCS in the HOL theorem prover (HOL4), with a focus towards the theory of unique solutions of contractions. (The formalisation consists of about 20,000 lines of proof scripts in Standard ML.) Some refinements of the theory itself are obtained. In particular we remove the constraints on summation, which must be weakly-guarded, by moving to rooted contraction, that is, the coarsest precongruence contained in the contraction preorder.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
