《謂詞邏輯與模型檢驗中的計量化理論》是依託陝西師範大學，由周紅軍擔任項目負責人的面上項目。
基本介紹
- 中文名：謂詞邏輯與模型檢驗中的計量化理論
- 項目類別：面上項目
- 項目負責人：周紅軍
- 依託單位：陝西師範大學
項目摘要,結題摘要,
項目摘要
由項目申請人提出的計量邏輯學已經在包括二值命題邏輯和各種多值命題邏輯中形成了較為完整的理論體系，為在各種邏輯系統中展開近似推理奠定了邏輯基礎.在表達能力更強的模態邏輯和謂詞邏輯中，申請人團隊也已開始了初步的研究，並通過隨機化和格值化等方法擴展了計量邏輯學的涵蓋範圍.在此基礎上，本項目提出的研究目標是：第一，在一階謂詞邏輯的框架下建立系統的計量邏輯理論，並用於解決Horn子句型資料庫相容性的估計問題；第二，線性時態邏輯（LTL）和計算樹邏輯（CTL）有比命題邏輯強的表述能力，也是模型檢驗理論用來表述規範（Specification）的主要工具.值得注意的是，滿足給定規範的遷移系統並不唯一，如何尋求極小的遷移系統以降低計算複雜度有重要意義.本項目將在上述兩種時態邏輯中建立起計量化理論，提出一個遷移系統對於給定規範的滿足度和冗餘度概念，最終找出滿足給定規範的最佳遷移系統 。
結題摘要
謂詞邏輯以及模型檢驗都具有比命題邏輯更強的表達能力，是人工智慧領域中的核心研究課題之一。基於賦值集上的均勻機率測度建立的命題邏輯的計量化理論是本項目申請時機率與邏輯交叉領域中具有代表性的研究成果。本項目以提高命題型計量邏輯的語言表達能力和邏輯推理能力為出發點，將在命題邏輯框架下成功建立起的計量化方法推廣到一階謂詞邏輯，線性時態邏輯及計算樹邏輯中，利用有限模型上的均勻機率測度建立相應的計量邏輯理論。首先，在不含函式符號的一階謂詞邏輯中，建立了系統的公理化真度理論；證明了該真度相對於解釋域的獨立性和可計算性；討論了全體真度值在單位閉區間[0,1]中的分布；引入了公式之間相似度和偽距離的計算方法；提出了邏輯形式理論的相容度理論；特別是證明了邏輯閉公式的真度之集與二值命題邏輯中的計算結果相一致,並且所有閉文字的真度都等於1/2；作為套用，給出了估計Horn 子句型資料庫相容度的一種方法；在更為精細的指標下討論了三 I 算法的魯棒性，從而較為系統地構建了謂詞邏輯的計量化理論。其次，針對若干重要的謂詞邏輯片段，建立了模態邏輯和線性時態邏輯的滿足度理論；研究了其邏輯公式的範式表示和計數問題，指出存在特徵的LTL公式在模型檢驗中總可以在有限步內判斷其有效性，即使相應的遷移系統含有無限多個狀態也是如此；構造了線性時序邏輯基於DTMC的計量化方法；更進一步將計量邏輯中的邏輯度量空間方法推廣到模糊集上，為模糊推理建立了邏輯基礎，從而較細緻地建立了模型檢驗的計量化理論。 本項目已順利完成當初擬定的研究計畫，項目組在科學出版社出版專著1部，系統總結和論述了命題型計量邏輯的機率隨機化及其套用方面的研究成果；正式發表標註該基金資助的研究論文32篇，其中SCI收錄8篇，EI收錄4篇，會議論文6篇。項目組成員1人晉升教授職稱，3人晉升副教授或副研究員，1人考取博士，目前在讀；培養博士生4人(含新招收博士2人)，其中3人已取得博士學位，1人已通過博士答辯，學位正在公示中。
