Maslov's Class K Revisited

Hustadt, U. and Schmidt, R. A. (1999)

In H. Ganzinger (ed.), Automated Deduction: CADE-16, Lecture Notes in Artificial Intelligence, Vol. 1632, Springer. BiBTeX, PostScript (Copyright © 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.


Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 27 Apr 2001
Copyright © 1999 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk