| 模态逻辑推理的翻译方法 |
| |
| 引用本文： | 张健.模态逻辑推理的翻译方法[J].计算机研究与发展,1998,35(5):389-392. |
| |
| 作者姓名： | 张健 |
| |
| 作者单位： | 中国科学院院软件研究所 |
| |
| 基金项目： | 国家自然科学基金,“863”高技术计划,中国科学院留学经费 |
| |
| 摘 要： | 文中研究了模态逻辑推理的翻译法，即把模态逻辑公式按照一定的规则翻译成经典逻辑公式，再用传统的定理器进行推理，文中指出，该方法在理论上保持了正规命题模态逻辑的可判定性，还给出了一些试验结果，说明该方法实际可行的。
|
| 关 键 词： | 自动定理证明 可满足性判定 模态逻辑推理 |
A TRANSLATION APPROACH TO MODAL LOGIC REASONING |
| |
| Zhang Jian.A TRANSLATION APPROACH TO MODAL LOGIC REASONING[J].Journal of Computer Research and Development,1998,35(5):389-392. |
| |
| Authors: | Zhang Jian |
| |
| Abstract: | A translation approach to modal logic reasoning is studied.This method tries to prove a modal theorem by translating it into a formula in the classic logic, and then proves the formula by using a conventional theorem prover. It is pointed out that the translation approach preserves the decidability of propositional normal modal logics.Some experimental results are also given,which show that the method is practical. |
| |
| Keywords: | propositional modal logic automated theorem proving satisfiability decision |
| 本文献已被 CNKI 维普 等数据库收录！ |
