[發(fā)明專利]一種一階并行、帶優(yōu)先級和逐點(diǎn)的限定理論計算方法

在審

• 申請?zhí)枺?/td>: 201510097186.1
• 申請日: 2015-03-04
• 公開（公告）號: CN104750974A
• 公開（公告）日: 2015-07-01
• 發(fā)明（設(shè)計）人: 萬海;蕭展豪;曾娟
• 申請（專利權(quán)）人: 中山大學(xué)
• 主分類號: G06F19/00
• 分類號: G06F19/00
• 代理公司: 廣州粵高專利商標(biāo)代理有限公司 44102
• 代理人: 林麗明

1.一種一階并行、帶優(yōu)先級和逐點(diǎn)的限定理論計算方法，其特征在于：用于將采用并行、帶優(yōu)先級和逐點(diǎn)的限定理論描述的問題翻譯成穩(wěn)定模型下的一階理論，在一般結(jié)構(gòu)下消去一階穩(wěn)定模型理論中的存在量詞，對優(yōu)化后的一階回答集邏輯程序調(diào)用回答集邏輯程序求解器進(jìn)行計算；具體包括以下步驟：

(1)將任意一個一階限定理論在線性時間內(nèi)翻譯為另一個與之在任意結(jié)構(gòu)上邏輯等價的在穩(wěn)定語義下的一階理論，包括四個基于語法層面的主要翻譯：從一階并行限定理論到一階穩(wěn)定理論、從若干個一階并行限定理論的合取到一階穩(wěn)定理論、從一階帶優(yōu)先級的限定理論到一階穩(wěn)定理論、從一階逐點(diǎn)限定理論到一階穩(wěn)定理論；

(2)采用消去量詞的優(yōu)化翻譯算法消去一階限定理論中的存在量詞；

(3)基于以上的翻譯和消去存在量詞優(yōu)化算法，將在限定理論語義下的一階理論最終轉(zhuǎn)化為回答集程序，通過調(diào)用回答集求解器，從而實(shí)現(xiàn)了一個能夠在給定的論域中求出所有極小模型的通用一階限定理論求解器。

2.根據(jù)權(quán)利要求1所述的一階并行、帶優(yōu)先級和逐點(diǎn)的限定理論計算方法，其特征在于：上述的一階并行限定理論到一階穩(wěn)定理論的翻譯具體是：通過對比一階并行限定理論與一階穩(wěn)定理論的定義，確定其具有近似的形式，即均邏輯等價于一個一階語句與一個二階語句的合取；則得到一階并行限定理論到一階穩(wěn)定理論的翻譯為如下公式：

Tr_v是能夠使原一階語句與翻譯后的一階語句具有相同的模型，讓原二階公式與翻譯后的二階公式等價，對原公式的翻譯不會影響的判斷，模擬能夠在論域中任意改變的可變謂詞變元

其中：1)為任意具有否定范式形式的一階語句，σ_m和σ_v表示兩個互不相交的謂詞常元集合，表示在原一階語句個體變元序列：x₁,x₂,…x_n；

2)是將中所有形如的正文字替換為后所得到的公式，P∈σ_m；是對按如下方法替換后得到的公式：將中所有形如的負(fù)文字替換為P∈σ_m；將中所有形如的正文字替換為Q∈σ_v；將中所有形如的負(fù)文字替換為Q∈σ_v；

3)0元謂詞γ是從未出現(xiàn)過的輔助謂詞，謂詞Q′是相應(yīng)于可變謂詞常元Q，Q∈σ_v引入的從未出現(xiàn)過的輔助謂詞，且每對Q和Q′具有相同的元數(shù)，謂詞集σ′_v表示由這些輔助謂詞Q′組成的集合。