人工智慧邏輯

是自動驗證最重要的方法之一。近年來，模型檢測技術與人工智慧的結合，成為一個研究的熱點。具體地，就是擴充或者修改模型檢測的時態邏輯，使之能夠刻畫多agents系統的特徵

時態邏輯模型檢測。互動時態邏輯(Alternating Time TemporalLogic) ,以下簡稱為ATL,是其中較為成功的框架。使用ATL,可以刻畫多個agents的相互合作,即, agents通過相互合作保證計算系統進入預定的某個(些)狀態。然而, agents之間的衝突,是現實計算系統的一個重要特徵。文章基於ATL,擴充其為一種表達力更強的時態邏輯,稱之為競爭互動時態邏輯(Competition Alternating Time TemporalLogic) ,簡稱為CATL。CATL的表達力,體現在它不僅可以刻畫agents的合作,也能夠刻畫agents相互的競爭。而且, CATL的表達力並沒有以提高計算複雜性為代價。人工智慧科學，從其誕生之日起便與邏輯學密不可分，二者的共同發展促進了用機器模仿人類思維的智慧型學的進步。