限定逻辑的表列方法

Tableau Methods of Circumscriptive Logic

限定逻辑是由McCarthy创立的非单调逻辑的一个重要分支。限定逻辑最大的困难在于其算法的设计。基于表列方法,可以给出命题限定逻辑和公式限定逻辑两种形式证明程序。

Circumscriptive logic is one of the most important branches of nonmonotonic logics which has been established by McCarthy. The most difficult problem of circumscriptive logic is to design an algorithm for it. Two kinds of formal proof procedure based on tableaux had been given for proposi- tional circumscriptive logic and formula circumscriptive logic.