量化带标公式的消解 (2009年)

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