U. Hustadt and R. A. Schmidt (1999a): ``Maslov's class K revisited.'' In H. Ganzinger, editor, Proceedings of the 16th International Conference on Automated Deduction (CADE-16) [Trento, Italy, 7-10 July 1999], pp. 172-186. LNAI 1632, Springer.
Abstract, BibTeX, PDF (© Springer).

This paper gives a new treatment of Maslov's class K in the framework of resolution. More specifically, we show that K and the class DK consisting of disjunction of formulae in K can be decided by a resolution refinement based on liftable orderings. We also discuss relationships to other solvable and unsolvable classes. [an error occurred while processing this directive]