中文摘要：

在引入量化单一带标公式的概念后，给出其消解算法，并证明该消解算法是健全的和拒绝性完备的。因此该算法可用于对量化单一带标公式进行理论上的研究，同时也可用于在实际应用中解决这类公式的可满足性问题。最岳，根据消解算法，得出一个可以在多项式时间内判定可满足性的量化单一带标公式的子类。

英文摘要：

After the introduction of quantified monosigned formulae, the resolution for them is investigated and proved to be sound and refutational complete. This kind of resolution can be used not only for theoretical studies but also for practical applications. As a result, a subclass of quantified monosigned formulae which can be solved the satisfiability problem in polynomial time is recognized.