概称句词项逻辑的树图判定算法  

A Tableau Algorithm for Term Logic of Generic Sentences

作　　者：周北海[1] 马丽[1] 

机构地区：[1]北京大学哲学系

出　　处：《逻辑学研究》2013年第4期1-16,共16页Studies in Logic

基　　金：国家社科基金重大项目"基于多学科视域的认知研究"(12&ZD119)

摘　　要：概称句的形式刻画研究始于人工智能。从条件蕴涵引入开始,到建立概称句词项逻辑的形式系统GAG和Gaa,关于概称句这一系列的研究主要是围绕概称句自身性质的探讨,以试图对于概称句推理给出更合理的形式刻画,而没有同时兼顾计算机应用方面的考虑。回归问题的初始,关于概称句的概念理论是否还可以用于计算机科学领域,是这一研究路线所面临的问题。首先要解决的问题是,根据GAG和Gaa模型,公式的可满足性是否有能行的判定方法。对此本文给出了基于GAG语义的树图判定算法,包括相应的可靠性,完备性等证明。The formal description research for generics began in the artificial intelligence field. This research began with the introduction of conditional implication. So far, the formal systems GAG and Gaa are established for the term logic of generics. Until now, the generic research only focused on the properties of generics, in order to propose some more rational formlism. At the same time, the aspect of computer application is ignored. Looking back to the original intent of generic research, whether the concept theory of generics can be used in the computer science is an issue of this research. The first ques- tion to be answered is whether there is any feasible decidable method for the formula satisfiability according to the GAG and Gaa models. This paper provides a tableau algorithm based on the GAG semantics. The concept theory makes the generic sentences known better, and the formlism more succinct. Because its semantics is in the basis of Montague＇s type semantics, there are four kinds of semantic objects. Furthermore, the symbol 〉 here also has the function of default reasoning. Its explanation differs from the set selection function in the con- ditional semantics, but is a enhanced version of that. All the above mentioned aspects increase the difficulty to set up the tableau algorithm. How to deal with these issues and figure out the tableau rules is the key to solve the problem. This paper provides a group of tableau rules and a decision program to determine the satisfiability of GAG formulae, meanwhile, a method to construct a GAG model from an open branch on a tableau is shown. The soundness and completeness of the tableau algorithm are also proved with respect to the satisfiability under the GAG semantics.

关 键 词：概称句 词项逻辑 树图算法 内涵逻辑 

分 类 号：B812[哲学宗教—逻辑学]