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