引用本文: | 贲可荣,陈火旺.PTL 证明器的实现技术[J].国防科技大学学报,1994,16(1):53-59.[点击复制] |
Ben Kerong,Chen Huowang.The Techniques of PTL Prover[J].Journal of National University of Defense Technology,1994,16(1):53-59[点击复制] |
|
|
|
本文已被:浏览 5589次 下载 5781次 |
PTL 证明器的实现技术 |
贲可荣, 陈火旺 |
(国防科技大学 电子计算机系 湖南 长沙 410073)
|
摘要: |
基于文 [10] 中的理论,我们用Turbo-Prolog 编程,在386 微机上成功地实现了命题时态逻辑定理的证明器。该证明器在处理next幂次、归纳、归结、◇(xΛy)、until 等方面,均有独到之处。这些方面,克服了以往工作的不足。证明器界面友好、速度快、能力强。 |
关键词: 时态逻辑,定理证明,自动推理 |
DOI: |
投稿日期:1993-02-23 |
基金项目:863 计划资助项目 |
|
The Techniques of PTL Prover |
Ben Kerong, Chen Huowang |
(Department of Computer Science,NUDT,Changsha 410073)
|
Abstract: |
Based on the theory of [10], the propositional temporal logic (PTL) prover has been implemented in Turbo-Prolog and runs on 386 microcomputers. The PTL prover has some original features in dealing with the power of next, induction, resolution, ◇(xΛy), until,The prover's many full-screen facilities make it easy to use. The prover appears to be of reasonable efficiency for most current examples. |
Keywords: Temporal logic,theorem proving,automated reasoning |
|
|
|
|
|