计算机应用与软件
計算機應用與軟件
계산궤응용여연건
COMPUTER APPLICATIONS AND SOFTWARE
2014年
8期
9-12,24
,共5页
Fisher-Ladner闭包%canonical model%R规则%可满足性%完备性
Fisher-Ladner閉包%canonical model%R規則%可滿足性%完備性
Fisher-Ladner폐포%canonical model%R규칙%가만족성%완비성
Fisher-Ladner closure%Canonical model%R-rule%Satisfiability%Completeness
模态逻辑是研究必然、可能及其相关概念的逻辑.模态公式的可满足性问题和证明系统的完备性问题是模态逻辑中的两个经典的问题.为了解决这两个问题,提出一个构造模态公式的canonical model的方法.通过这个方法,对于给定模态公式(φ),如果(φ)是可满足的,可以得到(φ)的一个canonical model;如果(φ)是不可满足的,可以得到(Γ)(φ)的证明.此外,还给出命题模态逻辑完备性的一个构造性证明方法.
模態邏輯是研究必然、可能及其相關概唸的邏輯.模態公式的可滿足性問題和證明繫統的完備性問題是模態邏輯中的兩箇經典的問題.為瞭解決這兩箇問題,提齣一箇構造模態公式的canonical model的方法.通過這箇方法,對于給定模態公式(φ),如果(φ)是可滿足的,可以得到(φ)的一箇canonical model;如果(φ)是不可滿足的,可以得到(Γ)(φ)的證明.此外,還給齣命題模態邏輯完備性的一箇構造性證明方法.
모태라집시연구필연、가능급기상관개념적라집.모태공식적가만족성문제화증명계통적완비성문제시모태라집중적량개경전적문제.위료해결저량개문제,제출일개구조모태공식적canonical model적방법.통과저개방법,대우급정모태공식(φ),여과(φ)시가만족적,가이득도(φ)적일개canonical model;여과(φ)시불가만족적,가이득도(Γ)(φ)적증명.차외,환급출명제모태라집완비성적일개구조성증명방법.
