人工智能邏輯

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