量化带标公式的消解

首先引入量化带标公式,然后研究了量化带标公式的消解并且证明其健全性和拒绝完备性.另外,还引入了二元消解并证明其针对正规量化带标公式(一个量化带标公式的子集)是健全的和拒绝完备的.最后证明如果正规量化带标公式的每一个子句如果最多包含两个文字,则该公式的可满足性问题是易解的.

Resolution for Quantified Signed Formulae

This paper is devoted to investigate the resolution for quantified signed formulae (signed formulae with quantifiers). First we introduce quantified signed formulae. Then we investigate resolution for quantified signed formulae and prove its soundness and refutational completeness. Also a restricted resolution (binary resolution) is introduced and proved to be sound and refutationally complete for a sub-classof quantified signed formulae which each formula is with regular signed formulae as matrices (regular quantified signed formulae). As a result, the subclass of regular quantified signed formulae, which each formula only contains clauses with at most two signed literals, is tractable.