一阶逻辑推理系统中有关量词推理规则的研究

王文龙

摘 要 通过对两种一阶逻辑自然推理系统中有关量词的推理规则及其成立条件的比较分析，给出形式简单、直观的有关量词的推理规则和合理、严谨的成立条件，从而保证在使用这些规则时，既保留了直观性，又消除了不严格性，并能准确把握成立条件.

关鍵词 一阶逻辑；全称量词；存在量词；推理规则；成立条件

中图分类号 TP301 O141 文献标识码 A 文章编号 1000-2537（2017）03-0089-06

Study of Inference Rules for Quantifiers in First-order Logic Inference System

WANG Wen-long1*， ZHANG Bo-feng2

（1.College of Computer Science and Technology， Kashgar University， Kashgar 844000， China；

2.School of Computer Engineering and Science， Shanghai University， Shanghai 200041， China）

Abstract Through the analysis of two inference rules for quantifiers and establishing conditions in first-order logic natural inference system， in this work， we establish intuitive inference rules for quantifiers with reasonable and strictly elaborated conditions. Not only these rules are intuitive and strict， but they also establish conditions that can accurately be grasped.

Key words first order logic； universal quantifier； existential quantifier； inference rules； establish condition

文献[1～12]描述了一阶逻辑自然推理系统中有关量词的推理规则，即全称量词引入规则、全称量词消去规则、存在量词引入规则、存在量词消去规则，在自然推理系统中具有重要作用.但由于使用这些推理规则时必须要满足一定条件，而这些条件不容易准确把握.另一方面，关于量词的推理规则，不同的自然推理系统会有不同的表示形式，使用这些规则的要求也有所不同.基于以上两方面因素，在使用量词的推理规则时，极易产生问题.因此，本文对两种一阶逻辑自然推理系统中有关量词的推理规则及其成立条件进行比较分析，并根据分析，阐述在使用这些推理规则过程中应采取的表示形式及成立条件，从而保证在使用这些规则时，既保留规则的直观性，又消除规则的不严格性，并能准确把握成立条件.