| 引用本文: | 贲可荣,陈火旺.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[点击复制] |
|
| |
|
|
| 本文已被：浏览 6049次 下载 6385次 |
| 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 |
|
|
|
|
|
