王文龍

摘 要 通過對(duì)兩種一階邏輯自然推理系統(tǒng)中有關(guān)量詞的推理規(guī)則及其成立條件的比較分析，給出形式簡單、直觀的有關(guān)量詞的推理規(guī)則和合理、嚴(yán)謹(jǐn)?shù)某闪l件，從而保證在使用這些規(guī)則時(shí)，既保留了直觀性，又消除了不嚴(yán)格性，并能準(zhǔn)確把握成立條件.

關(guān)鍵詞 一階邏輯；全稱量詞；存在量詞；推理規(guī)則；成立條件

中圖分類號(hào) TP301 O141 文獻(xiàn)標(biāo)識(shí)碼 A 文章編號(hào) 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

文獻(xiàn)[1～12]描述了一階邏輯自然推理系統(tǒng)中有關(guān)量詞的推理規(guī)則，即全稱量詞引入規(guī)則、全稱量詞消去規(guī)則、存在量詞引入規(guī)則、存在量詞消去規(guī)則，在自然推理系統(tǒng)中具有重要作用.但由于使用這些推理規(guī)則時(shí)必須要滿足一定條件，而這些條件不容易準(zhǔn)確把握.另一方面，關(guān)于量詞的推理規(guī)則，不同的自然推理系統(tǒng)會(huì)有不同的表示形式，使用這些規(guī)則的要求也有所不同.基于以上兩方面因素，在使用量詞的推理規(guī)則時(shí)，極易產(chǎn)生問題.因此，本文對(duì)兩種一階邏輯自然推理系統(tǒng)中有關(guān)量詞的推理規(guī)則及其成立條件進(jìn)行比較分析，并根據(jù)分析，闡述在使用這些推理規(guī)則過程中應(yīng)采取的表示形式及成立條件，從而保證在使用這些規(guī)則時(shí)，既保留規(guī)則的直觀性，又消除規(guī)則的不嚴(yán)格性，并能準(zhǔn)確把握成立條件.