逻辑学研究
邏輯學研究
라집학연구
SUN YATSEN UNIVERSITY FORUM
2012年
1期
11-34
,共24页
表达能力%逻辑%复杂性%SO%结构%证明%程序%版本
錶達能力%邏輯%複雜性%SO%結構%證明%程序%版本
표체능력%라집%복잡성%SO%결구%증명%정서%판본
本文研究了在所有有穷结构上SO.HORN*,SO—HORNτ和SO-HORNτ的表达能力。我们证明了SO-HORNτ,SO—HORN*τ和FO(LFP)的表达能力是一致的,SO—HORN*是SO-HORNτ的一个严格子逻辑。为了证明这一结果,我们提出了DATALOG*程序,DATALOGτ程序以及它们的分层版本S-DATALOG*程序利S-DATALOGτ程序。我们证明了在所有有穷结构上DATALOGτ和S-DATALOGτ是等价的,并且DATALOG。足DATALOGτ的一个严格子逻辑。最后我们还用两种方法证明了SO-HORN的一个扩展版本SO—EHORNτ逻辑可以在所有有穷结构有有结构上刻画co—NP。
本文研究瞭在所有有窮結構上SO.HORN*,SO—HORNτ和SO-HORNτ的錶達能力。我們證明瞭SO-HORNτ,SO—HORN*τ和FO(LFP)的錶達能力是一緻的,SO—HORN*是SO-HORNτ的一箇嚴格子邏輯。為瞭證明這一結果,我們提齣瞭DATALOG*程序,DATALOGτ程序以及它們的分層版本S-DATALOG*程序利S-DATALOGτ程序。我們證明瞭在所有有窮結構上DATALOGτ和S-DATALOGτ是等價的,併且DATALOG。足DATALOGτ的一箇嚴格子邏輯。最後我們還用兩種方法證明瞭SO-HORN的一箇擴展版本SO—EHORNτ邏輯可以在所有有窮結構有有結構上刻畫co—NP。
본문연구료재소유유궁결구상SO.HORN*,SO—HORNτ화SO-HORNτ적표체능력。아문증명료SO-HORNτ,SO—HORN*τ화FO(LFP)적표체능력시일치적,SO—HORN*시SO-HORNτ적일개엄격자라집。위료증명저일결과,아문제출료DATALOG*정서,DATALOGτ정서이급타문적분층판본S-DATALOG*정서리S-DATALOGτ정서。아문증명료재소유유궁결구상DATALOGτ화S-DATALOGτ시등개적,병차DATALOG。족DATALOGτ적일개엄격자라집。최후아문환용량충방법증명료SO-HORN적일개확전판본SO—EHORNτ라집가이재소유유궁결구유유결구상각화co—NP。
We study the expressive powers of SO-HORN*, SO-HORNτ and SO-HORN*r on all finite structures. We show that SO-HORNτ, SO-HORN*r, FO(LFP) coincide with each other and SO-HORN* is proper sublogic of SO-HORNr. To prove this result, we introduce the notions of DATALOG* program, DATALOGτ program and their stratified versions, S- DATALOG* program and S-DATALOGτ program. It is shown that, on all structures, DATALOGτ and S-DATALOGτ are equivalent and DATALOG* is a proper sublogic of DATALOGτ. SO-HORN* and SO-HORNτ can be treated as the negations of DATALOG* and DATALOGr, respectively. We also show that SO-EHORNτ logic which is an extended version of SO-HORN captures co-NP on all finite structures.