中山大学学报（自然科学版）
中山大學學報（自然科學版）
중산대학학보（자연과학판）
ACTA SCIENTIARUM NATURALIUM UNIVERSITATIS SUNYATSENI
2010年
1期
20-23
,共4页
量化单一带标公式%消解%可满足性%多项式时间可判定
量化單一帶標公式%消解%可滿足性%多項式時間可判定
양화단일대표공식%소해%가만족성%다항식시간가판정
quantified monosigned formulae%resolution%satisfiability%in polynomial time
在引入量化单一带标公式的概念后,给出其消解算法,并证明该消解算法是健全的和拒绝性完备的.因此该算法可用于对量化单一带标公式进行理论上的研究,同时也可用于在实际应用中解决这类公式的可满足性问题.最后,根据消解算法,得出一个可以在多项式时间内判定可满足性的量化单一带标公式的子类.
在引入量化單一帶標公式的概唸後,給齣其消解算法,併證明該消解算法是健全的和拒絕性完備的.因此該算法可用于對量化單一帶標公式進行理論上的研究,同時也可用于在實際應用中解決這類公式的可滿足性問題.最後,根據消解算法,得齣一箇可以在多項式時間內判定可滿足性的量化單一帶標公式的子類.
재인입양화단일대표공식적개념후,급출기소해산법,병증명해소해산법시건전적화거절성완비적.인차해산법가용우대양화단일대표공식진행이론상적연구,동시야가용우재실제응용중해결저류공식적가만족성문제.최후,근거소해산법,득출일개가이재다항식시간내판정가만족성적양화단일대표공식적자류.
