逻辑学研究
邏輯學研究
라집학연구
Supplement to the Journal of Sun Yatsen University
2012年
1期
11~34
,共null页
表达能力 逻辑 复杂性 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.
