畢業(yè)設(shè)計(jì)（論文）文獻(xiàn)譯文：強(qiáng)等價(jià)邏輯編程

畢業(yè)設(shè)計(jì)（論文）--文獻(xiàn)翻譯原文題目StronglyEquivalentLogicPrograms譯文題目強(qiáng)等價(jià)邏輯專業(yè)信息與計(jì)算科學(xué)姓名學(xué)號(hào)指導(dǎo)教師強(qiáng)等價(jià)邏輯編程VLADIMIRLIFSCHITZUniversityofTexasDAVIDPEARCEEuropeanCommissionandAGUSTINVALVERDEUniversityofMalaga摘要邏輯程序Π1被認(rèn)為等價(jià)于在答案集上的邏輯程序Π2，如果Π1和Π2具有相同的答案集的語義。對(duì)于每個(gè)邏輯程序Π，Π1Π和Π2Π具有相同的答案集。研究強(qiáng)等價(jià)性很重要，因?yàn)槲覀儚闹袑W(xué)到了如何簡(jiǎn)化邏輯的一部分程序，但還并不完善。主要定理表明，驗(yàn)證強(qiáng)等價(jià)性可以通過檢查單調(diào)邏輯中公式的等價(jià)性來實(shí)現(xiàn)，此處的邏輯是古典邏輯和直覺主義之間的邏輯。類別和主題描述符：F.4.1[數(shù)學(xué)邏輯]：邏輯編程邏輯編程一般條款：語言，理論附加關(guān)鍵詞和短語：答案集，邏輯編程，穩(wěn)定模型

4.3直覺邏輯論程序的例子（4）和（5）表明，在這兩處中邏輯定理1的陳述不能被直覺邏輯所取代：這些程序是強(qiáng)等價(jià)，但不直觀的等效。程序（4）在語法上是相當(dāng)復(fù)雜的：它包含一個(gè)析取規(guī)則和約束。但我們可以給出一個(gè)類似的反例不使用規(guī)則這些。如下程序q←notpp←notqr←p,q(12)s←ps←q通過添加規(guī)則獲得（12）的程序s←notr(13)可以證明使用克里普克模型這些項(xiàng)目并不是互相等效的直觀的。但它們是強(qiáng)等價(jià)的。從獲得的r→sp→qq→p(p∧q)→r(14)p→sq→s在HT，假設(shè)R使用公式第三（14）和德摩根定律，我們得到p∨q.：使用第一個(gè)公式（14），我們得到的p∨q問：使用最后兩個(gè)公式（14），我們推導(dǎo)出s。4.4平衡邏輯為證明主要定理，我們將利用一些結(jié)果非單調(diào)推理稱為平衡邏輯。平衡邏輯可以描述為HT邏輯中的一種特殊的最小模型推理，理論0的均衡模型是一個(gè)整體HT，如下考慮，例如，理論包括一個(gè)單一的原子公式p.其模型在邏輯HT上是<{p},{p}><{p},{p,q}><{p,q},{p,q}>首先是均衡模型。第二個(gè)不是，因?yàn)樗皇峭暾?。第三也不是均衡模型，因?yàn)樗粷M足最小條件（II）。另一個(gè)例子是，這個(gè)模型屬于HT邏輯：<,{p}><{p},{p}>這也不是均衡模型：第一個(gè)它不完整，第二個(gè)不是最小。事實(shí)上，這一理論沒有均衡模型。引理1。對(duì)于任何沒有失敗的程序，都是一個(gè)HT模型<IH,IT>。而在HT模型中得到解釋，在HT模型上，Head←Body是一個(gè)經(jīng)典模型。<IH,IT,H>|=Bodyimplies<IH,IT,H>|=Head <IH,IT,T>|=Bodyimplies<IH,IT,T>|=Head因?yàn)椴话穸ǎ@些條件可以簡(jiǎn)化如下：IH|=BodyimpliesIH|=HeadIT|=BodyimpliesIT|=Head為每一條規(guī)則要求head←body這個(gè)規(guī)則，也就是要求其在古典邏輯的意義上是以上模型。引理2。一個(gè)HT解釋下符合<IH,IT>，那么它產(chǎn)生于。引理的證明使用了兩個(gè)可以很容易通過結(jié)構(gòu)進(jìn)行驗(yàn)證的事實(shí)歸納。一是對(duì)“單調(diào)性”的解釋:例1對(duì)任何HT解釋法下的<IH,IT>和任何命題公式F，如果<IH,IT,H>|=F然后<IH,IT,T>|=F。另一種則關(guān)系到HT滿意度關(guān)系的古典邏輯:例2對(duì)于任何HT解釋下的<IH,IT>和任何命題公式F，如果<IH,IT,T>|=F那么IT|=F.證明引理2。根據(jù)還原(第3部分)的定義，是由同時(shí)替換一些的程序獲得的程序最大的子公式形式不是⊥相關(guān)的F，和所有其他與⊥相關(guān)形式。它有足夠的自檢性，對(duì)于任何最大值子公式，notF可以替換它的公式G，<IH,IT>|=notFiff<IH,IT>|=G由于G不是⊥，也可寫作<IH,IT>|=notFiffG=⊥這個(gè)等價(jià)的左邊是iff<IH,IT,H>|≠Fand<IH,IT,T>|≠F結(jié)合實(shí)例1，第一項(xiàng)就是第二項(xiàng)的結(jié)論，所以也可以被刪除。結(jié)合實(shí)例2，第二項(xiàng)可以寫為IT|≠F,它是G=⊥的條件。因?yàn)?lt;IT,IT>滿足每一個(gè)公式,它是一個(gè)∪的模型?？梢钥闯鏊幱谄胶鉅顟B(tài),在考察任何模型時(shí)<J,IT>，∪是IT子集。顯然J必須包含IT。但它不能等于IH，因?yàn)榧僭O(shè)<IH，IT>，H?J?T。用一個(gè)原子A∈J\IH和原子B∈IT\J.這些原子，A→B屬于。但<J,IT>不滿足這個(gè)含義，與它是a的假設(shè)相反。最后，可證<IH，IT>不是一個(gè)平衡模型。因此，T的任何一個(gè)合適的子集，都不是一個(gè)均衡模型∪。

五．增加第二否定答案集通常定義為具有第二種類型的邏輯程序否定，表示一個(gè)原子的直接或明確的否定。在gelfond以及Lifschitz[1991]和Lifschitzetal.[1999]，這第二個(gè)否定被稱為“古典”,可以理解是命題原子或原子前綴。我們定義擴(kuò)展公式、擴(kuò)展規(guī)則和擴(kuò)展程序我們?cè)谏厦娴牡?部分中定義了公式、規(guī)則和程序，任意的字符可以代替原子。語義擴(kuò)展程序定義的是一個(gè)一致的集合X是一個(gè)答案集擴(kuò)展程序，詳細(xì)信息見Lifschitzetal.[1999]。對(duì)邏輯程序的語法添加第二個(gè)否定是很重要的。但在實(shí)際應(yīng)用上，計(jì)算上，這個(gè)擴(kuò)展并不是很重要。事實(shí)上，第二個(gè)否定可以通過一個(gè)簡(jiǎn)單的語法轉(zhuǎn)換從程序中消除。對(duì)每個(gè)原子A的基礎(chǔ)語言，選擇一個(gè)新的原子。例如，如果是p;pq←p(15)q是p;q←p(16)⊥←p,⊥←q,(假設(shè)底層語言中除了p和q之外沒有原子)只有答案集(15){p};因此,唯一的答案由(16)得{}。關(guān)于程序的強(qiáng)等價(jià)性的問題也出現(xiàn)在這個(gè)問題上擴(kuò)展問題。例如，它在Erdem和Lifschitz(1999)中顯示，在任何擴(kuò)展程序中，分隔規(guī)則p;p(17)可以等價(jià)地用兩個(gè)非分隔規(guī)則替代p←notp?p←notp(18)下面的定理允許我們減少對(duì)擴(kuò)展程序的強(qiáng)等價(jià)性的驗(yàn)證，以檢查公式的HT等價(jià)性。例如，要看，(17)和(18)就足夠檢查HT的等效性圖1所示。邏輯程序語言與命題語言之間的對(duì)應(yīng)關(guān)系存在兩個(gè)否定的公式。p←not←notp⊥←p,但這些都是在介紹中討論過的項(xiàng)目(4)和(5)代替q，重寫為一組命題公式，這兩個(gè)程序變成(6)和(7)，在第二節(jié)，我們已經(jīng)證明了它是等價(jià)的。命題公式識(shí)別公式和規(guī)則延伸它們,我們可以把第二否定寫作～。在之間的對(duì)應(yīng)了關(guān)系邏輯程序的語言和命題公式的語言，圖1總結(jié)了兩個(gè)否定的存在。我們的主要定理很容易概括為新的設(shè)置(證明的方法是完全相同的)，我們可以證明兩個(gè)擴(kuò)展的程序是強(qiáng)等價(jià)的，當(dāng)且僅當(dāng)它們?cè)谶壿婲5中是等價(jià)的。有趣的是，從本節(jié)開始討論的擴(kuò)展程序中消除第二個(gè)否定的方法可以推廣到N5。對(duì)于N5語言中的任何公式F，都有一個(gè)相當(dāng)于“減少”的公式r(F)的第二否定象征～，這樣它就可以直接站在一個(gè)原子的前面[Vorob'ev1964]。考慮一下消除第二否定的句法轉(zhuǎn)換，公式F通過替換每個(gè)部分的形式～r(F)和一個(gè)新的原子的形式。這類似于由古雷維奇(1977年)提出的直覺邏輯Nelson強(qiáng)烈否定的邏輯。

6結(jié)論有關(guān)邏輯程序的強(qiáng)等價(jià)性的事實(shí)告訴我們，如何在不查看其他部分的情況下簡(jiǎn)化邏輯程序的一部分。強(qiáng)等價(jià)性可以用各種各樣的邏輯來描述。這一邏輯的理論集合包括所有直觀的可命題公式，被排除的中間弱法則，以及德摩根的定律。兩個(gè)程序是強(qiáng)等價(jià)的這一事實(shí)通?？梢酝ㄟ^推導(dǎo)得到彼此使用這些邏輯方法。這里有一個(gè)指數(shù)時(shí)間算法用來驗(yàn)證強(qiáng)等價(jià)。Reiter和Gelfond的擴(kuò)展的非分隔程序的定義是：這一觀點(diǎn)認(rèn)為，這些程序只不過是Gelfond的默認(rèn)理論的一個(gè)特例。默認(rèn)值是推理規(guī)則的泛化：除了前提和結(jié)論，違約有“理由”。因此，邏輯符號(hào)←是程序類似于將結(jié)論與前提相分離的方法推理規(guī)則。在