Rules of Inference for Quantifiers in Discrete Mathematics
-
摘要: 清楚地叙述了自然推理系统中的存在量词消去规则和全称量词引入规则满足的条件,而这些条件在许多离散数学教科书中叙述得相当含糊.与某些教科书中存在量词消去规则只能用于无自由变元的公式不同,按照本文给出的条件,存在量词消去规则也可以用于有自由变元的公式,因而增强了系统的推理能力.引进了解释之间和赋值之间关于公式集的等价性,从而证明了系统是可靠的,即一个证明中的结论是其前提的逻辑推论.Abstract: The conditions satisfied for the existential instantiation and the universal generalization in the natural deduction system are described clear, whereas they are described rather vaguely in many textbooks on discrete mathematics. Contrasting with that the existential instantiation in some textbooks is used only for formulas without free variables, according to the condition we given, it may be also used for formulas with free variables and the ability to reason has increased. Introducing the equivalence between interpretations and the equivalence between assignments with respect to a set of formulas, it is proved that the system is sound, that is, in a proof, the conclusion is a logical consequence of the premises.
-
Key words:
- predicate logic /
- logical systems /
- discrete mathematics /
- soundness /
- quantifier
-
[1] 陈进元,屈婉玲.离散数学(上)[M].北京:北京大学出版社,1987. [2]左孝凌,李为鉴,刘永才.离散数学[M].上海:上海科学技术文献出版社,1982. [3]王遇科.离散数学[M].北京:北京理工大学出版社,1986. [4]蔡高火.离散数学基础[M].桂林:广西师范大学出版社,1992. [5]Stanat D F, Mcallister D F. Discrete mathematics in computer science[M]. Englewood Cliffs:Prentice Hall, 1977. [6]胡世华,陆钟万.数理逻辑基础[M].北京:科学出版社,1981. [7]尹宝林,何自强,许光汉,等.离散数学[M].北京:高等教育出版社,1998. [8]檀凤琴,何自强.离散数学[M].北京:科学出版社,1999.
点击查看大图
计量
- 文章访问数: 3551
- HTML全文浏览量: 70
- PDF下载量: 1131
- 被引次数: 0