| 开放逻辑及其实现技术 |
| |
| 引用本文： | 汪亚文,李未.开放逻辑及其实现技术[J].北京航空航天大学学报,1992(3):122-129. |
| |
| 作者姓名： | 汪亚文 李未 |
| |
| 作者单位： | 北京航空航天大学计算机科学与工程系
(汪亚文)，北京航空航天大学计算机科学与工程系(李未) |
| |
| 摘 要： | 定义了一个建立在一阶谓词基础上的开放的逻辑系统,它由证明演算和假设演算组成。本文在文献1]的基础之上对假设演算进行了某些扩充,使得假设演算中所构造的删除规则集是完备的;并说明了对任一语句的可判定性。为便于机器实现,文中引入了删除推演序列的概念;并给出了如何构造删除规则的与或树以及如何生成删除推演序列的步骤。最后,讨论了开放逻辑系统的具体实现技术。
|
| 关 键 词： | 证明演算 假设演算 反例 反驳 |
AN OPEN LOGIC SYSTEM AND ITS IMPLEMENTATION |
| |
| Wang Yawen Li Wei.AN OPEN LOGIC SYSTEM AND ITS IMPLEMENTATION[J].Journal of Beijing University of Aeronautics and Astronautics,1992(3):122-129. |
| |
| Authors: | Wang Yawen Li Wei |
| |
| Institution: | Dept. of Computer Sci. and Eng. |
| |
| Abstract: | An open logic system,which consists of proof calculus and hypothesis calculus,is constructed in this papaer.The hypothesis calculus is expanded to make the removal ruleset complete.The concept of removal induction sequent is introduced.Steps are given to construct the and-or-trees of removal rules and to generate the removal induction sequents. |
| |
| Keywords: | proof calculus hypothesis calculus counter example refutation removal rule induction sequent and-or-tree |
| 本文献已被 CNKI 维普 等数据库收录！ |
