Resolution for Quantified Monosigned Formulae
Jin Jiwei, Xishun Zhao · Acta Scientiarum Naturalium Universitatis Sunyatseni · 2010
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.