| 面向传值进程的谓词μ-演算与FO(HML)的完备推演系统 |
| |
| 引用本文： | 薛锐,林惠民.面向传值进程的谓词μ-演算与FO(HML)的完备推演系统[J].计算机学报,2002,25(6):561-569. |
| |
| 作者姓名： | 薛锐 林惠民 |
| |
| 作者单位： | 中国科学院软件研究所计算机科学实验室,北京,100083 |
| |
| 基金项目： | 国家自然科学基金 (6983 3 0 2 0 )，山西省归国留学生基金，中国科学院软件研究所开放实验室青年科学基金资助 |
| |
| 摘 要： | 作者提出一个谓词μ－演算系统，目的在于描述传值进程的性质，该系统的公式和谓词相互递归定义，谓词中含有抽象式，谓词变元以及最大和最小不动点，其语义模型是带赋值的符号迁移图所诱导的迁移系统，并且该系统包含Hennessy-Milner逻辑的一阶扩弃FO（HML）作为子系统，作者用例说明了本演算系统在表达传值进程性质方面的优越性，该文后半部分主要给出了FO（HML）的一个推演系统，并运用判定树（Tableau)的方法，证明了所给出了推演系统是完备的。
|
| 关 键 词： | 传值进程 谓词μ－演算 FO 完备推演系统 计算机 |
| 修稿时间： | 2000年10月13 |
A Predicate μ-Calculus for Value-Passing Processes and A Complete Deductive System for FO(HML) |
| |
| XUE Rui,LIN Hui,Min.A Predicate μ-Calculus for Value-Passing Processes and A Complete Deductive System for FO(HML)[J].Chinese Journal of Computers,2002,25(6):561-569. |
| |
| Authors: | XUE Rui LIN Hui Min |
| |
| Abstract: | |
| |
| Keywords: | Tableau |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
