证明策略的集成研究

证明策略的集成研究 Study on Integrated Proof Strategy 何锫 HE Pei 1 first-author 姚跃华 YAO Yue\|hua 1 叶吉祥 YE Ji\|xiang 1 长沙交通学院计算机科学系,长沙,410076 长沙交通学院计算机科学系,长沙,410076 Departmemt of Computer Science, Changsha Communications Institute Departmemt of Computer Science, Changsha Communications Institute 讨论了ＸＹＺ／ＶＥＲＩ系统的向后推理机制，具体而言是基本策略、集成策略语言、策略的结构以及在这样的策略集成环境中的向后推理过程． XYZ/VERI is an interactive computer aided proof system for temporal logic and XYZ/SE program’s verifications. This paper discusses its backward deduction mechanism, that is, its basic tactics, integrated tactic language, tactic’s structure, and backward deductions in the integrated tactic environment like XYZ/VERI system. 证明策略 集成策略语言 向后推理 proof strategy integrated tactic language backward deduction TP311 1999-05-01 2021-04-01 5