计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2014年
3期
205-211
,共7页
李屾%常亮%孟瑜%李凤英
李屾%常亮%孟瑜%李鳳英
리신%상량%맹유%리봉영
时态描述逻辑%分支时态逻辑%可满足性问题%Tableau算法%复杂度
時態描述邏輯%分支時態邏輯%可滿足性問題%Tableau算法%複雜度
시태묘술라집%분지시태라집%가만족성문제%Tableau산법%복잡도
Temporal description logic%Branching temporal tree logic%Satisfiability problem%Tableau algorithm%Complexity
时态描述逻辑是将描述逻辑与时态逻辑相结合后得到的逻辑系统,具有较强的描述能力;但是大部分的时态描述逻辑都是将时态算子同时引入到概念和公式中,使得公式可满足性问题的计算复杂度过高.将描述逻辑ALC与分支时态逻辑CTL相结合,提出新的分支时态描述逻辑ALC-CTL.该逻辑没有将时态算子用于概念的构造过程,而是将时态算子引入到公式的构造中;从分支时态逻辑的角度看,相当于将CTL中的原子命题提升为描述逻辑中的个体断言.最终得到的逻辑系统不仅具有较强的刻画能力,还使得公式可满足性问题的复杂度保持在EXPTIME-完全这个级别.通过将CTL的Tableau判定算法与描述逻辑ALC的推理机制有机结合,给出了ALC-CTL的Tableau判定算法并证明了算法的可终止性、可靠性和完备性.
時態描述邏輯是將描述邏輯與時態邏輯相結閤後得到的邏輯繫統,具有較彊的描述能力;但是大部分的時態描述邏輯都是將時態算子同時引入到概唸和公式中,使得公式可滿足性問題的計算複雜度過高.將描述邏輯ALC與分支時態邏輯CTL相結閤,提齣新的分支時態描述邏輯ALC-CTL.該邏輯沒有將時態算子用于概唸的構造過程,而是將時態算子引入到公式的構造中;從分支時態邏輯的角度看,相噹于將CTL中的原子命題提升為描述邏輯中的箇體斷言.最終得到的邏輯繫統不僅具有較彊的刻畫能力,還使得公式可滿足性問題的複雜度保持在EXPTIME-完全這箇級彆.通過將CTL的Tableau判定算法與描述邏輯ALC的推理機製有機結閤,給齣瞭ALC-CTL的Tableau判定算法併證明瞭算法的可終止性、可靠性和完備性.
시태묘술라집시장묘술라집여시태라집상결합후득도적라집계통,구유교강적묘술능력;단시대부분적시태묘술라집도시장시태산자동시인입도개념화공식중,사득공식가만족성문제적계산복잡도과고.장묘술라집ALC여분지시태라집CTL상결합,제출신적분지시태묘술라집ALC-CTL.해라집몰유장시태산자용우개념적구조과정,이시장시태산자인입도공식적구조중;종분지시태라집적각도간,상당우장CTL중적원자명제제승위묘술라집중적개체단언.최종득도적라집계통불부구유교강적각화능력,환사득공식가만족성문제적복잡도보지재EXPTIME-완전저개급별.통과장CTL적Tableau판정산법여묘술라집ALC적추리궤제유궤결합,급출료ALC-CTL적Tableau판정산법병증명료산법적가종지성、가고성화완비성.
