《可計算性邏輯中若干Cirquent演算系統的研究》是依託西安電子科技大學，由許文艷擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：可計算性邏輯中若干Cirquent演算系統的研究
- 項目類別：青年科學基金項目
- 項目負責人：許文艷
- 依託單位：西安電子科技大學
中文摘要,結題摘要,
中文摘要
可計算性邏輯(CoL)是新近提出的關於可計算性的形式理論。它採取互動的博弈語義，同時也是一種資源邏輯。相比於傳統邏輯，CoL具有表達能力強、證明效率高的優點，這使得它在知識庫系統、人工智慧行為規劃、電路等價性驗證等領域有著良好的套用前景和廣闊的發展空間。Cirquent演算是CoL理論中的重要研究方法，其最大特點是允許分享子結構和採用深度推理，這是CoL理論具有上述優點的主要原因所在。因此，本項目擬對CoL中若干Cirquent演算系統進行研究，具體內容如下：(1)研究CoL不同邏輯部分相應的Cirquent演算系統；(2)研究若干Cirquent演算系統的證明複雜度問題；(3)給出多根Cirquent的定義及推理系統以套用於電路等價性驗證和最佳化等問題中。本項目研究課題新穎、方法獨特、內容詳實，在計算機科學、電路設計等領域有著重要的理論指導意義和套用價值。
結題摘要
可計算性邏輯(CoL)是新近提出的關於可計算性的形式理論。它採取互動的博弈語義，同時也是一種資源邏輯。相比於傳統邏輯，CoL具有表達能力強、證明效率高的優點，這使得它在知識庫系統、人工智慧行為規劃、電路等價性驗證等領域有著良好的套用前景和廣闊的發展空間。Cirquent演算是CoL理論中的重要研究方法，其最大特點是允許分享子結構和採用深度推理，這是CoL理論具有上述優點的主要原因所在。本項目對CoL理論中的若干Cirquent演算系統進行了研究，具體內容如下：(1)研究帶有Cluster的Cirquent演算系統；(2)研究同時帶有Cluster和Rank的Cirquent演算系統；(3)研究帶有復發運算元的Cirquent演算系統的可判定性；(4)研究多根Cirquent演算系統在電路等價性驗證與最最佳化問題中的套用。經過項目組成員的共同努力, 我們對上述研究內容取得的重要成果總結如下：(1)建立了帶有∨-Cluster的Cirquent演算公理系統，使IF邏輯命題部分得到了真正意義上的公理化；(2)建立了帶有∨-Cluster和2個Rank的Cirquent演算公理系統，解決了Extended IF邏輯命題水平的公理化問題；(3)建立了帶有∧,∨-Cluster和任意有限個Rank的Cirquent演算公理系統，為Extended IF邏輯命題部分提供了一個保守擴張系統，它是我們前期提出的兩個Cirquent演算系統的擴張，因此具有重要的理論和套用價值；(4)證明了帶有復發運算元的Cirquent演算系統CL15的可判定性。
