摘要
定义了一个建立在一阶谓词基础上的开放的逻辑系统,它由证明演算和假设演算组成。本文在文献[1]的基础之上对假设演算进行了某些扩充,使得假设演算中所构造的删除规则集是完备的;并说明了对任一语句的可判定性。为便于机器实现,文中引入了删除推演序列的概念;并给出了如何构造删除规则的与或树以及如何生成删除推演序列的步骤。最后,讨论了开放逻辑系统的具体实现技术。
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.
出处
《北京航空航天大学学报》
EI
CAS
CSCD
北大核心
1992年第3期122-129,共8页
Journal of Beijing University of Aeronautics and Astronautics
关键词
证明演算
假设演算
反例
反驳
proof calculus,hypothesis calculus,counter example,refutation,removal rule,induction sequent,and-or-tree.
