@INPROCEEDINGS{HustadtSchmidt99a,
AUTHOR = {Hustadt, U. and Schmidt, R. A.},
YEAR = {1999},
TITLE = {Maslov's Class {K} Revisited},
EDITOR = {Ganzinger, H.},
BOOKTITLE = {Automated Deduction---CADE-16},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {1632},
PUBLISHER = {Springer},
PAGES = {172--186},
ISBN = {3-540-66222-7},
URL = {http://www.cs.man.ac.uk/~schmidt/publications/HustadtSchmidt99a.html},
ABSTRACT = {This paper gives a new treatment of Maslov's class $\mathrm{K}$ in the 
framework of resolution. 
More specifically, we show that $\mathrm{K}$ and the class
$\mathrm{DK}$ consisting of disjunction of formulae in $\mathrm{K}$
can be decided by a resolution refinement based on liftable
orderings. We also discuss relationships to other solvable and
unsolvable classes.},
}