本文選題：非正規(guī)時(shí)序邏輯　切入點(diǎn)：公理系統(tǒng)　出處：《中國(guó)科學(xué):信息科學(xué)》2017年01期

【摘要】：本文對(duì)關(guān)系語義(或Kripke語義)下極小非正規(guī)模態(tài)邏輯C2進(jìn)行時(shí)序化處理,得到極小非正規(guī)時(shí)序邏輯C2t,并建立了C2t的Hilbert式公理系統(tǒng)HC2t,證明了其可靠性和完全性,C2t比極小時(shí)序邏輯Kt更具有一般性.本文還從證明論的角度對(duì)C2t進(jìn)行了研究,建立了C2t的一個(gè)加標(biāo)矢列式演算系統(tǒng)GC2t,并且證明了GC2t的可靠性和完全性,同時(shí)還證明了GC2t的切割消除定理(cut elimination),然后得到C2t的可判定性.在GC2t中還可以進(jìn)行證明搜索.
[Abstract]:In this paper, the minimal informal modal logic C2 under relational semantics (or Kripke semantics) is sequenced. The minimal informal sequential logic C2t is obtained, and the Hilbert axiomatic system HC2t is established. It is proved that the reliability and completeness of C2t are more general than that of minimal temporal logic Kt. In this paper, we also study C2t from the point of view of proof theory. A scalar vector calculus system GC2t of C2t is established, and the reliability and completeness of GC2t are proved. At the same time, the cut elimination theorem of GC2t is proved, and the determinability of C2t is obtained.
【作者單位】： 西南大學(xué)邏輯與智能研究中心;河南師范大學(xué)計(jì)算機(jī)與信息工程學(xué)院;西南大學(xué)計(jì)算機(jī)與信息科學(xué)學(xué)院;
【基金】：國(guó)家社會(huì)科學(xué)基金項(xiàng)目(批準(zhǔn)號(hào):16CZX049)資助
【分類號(hào)】：O141
，

本文編號(hào)：1658651