to De Nivelle, Schmidt and Hustadt (2000),
Resolution-Based Methods for Modal Logics,
Journal of the IGPL
8 (3) 265-292.
A condensation D of a clause C is a minimal multiple factor
of C which subsumes C.
A clause is condensed if there is no proper subclause of C which
is a factor of C.
Page 278, Replace (i) in definition of resolution with maximal selection
\sigma is the most general unifier of A1 \/ ... \/ An and
-An+1 \/ ... \/ -A2n such that Ai\sigma = An+1\sigma.
Page 278, (iii) in definition of resolution with maximal selection:
Replace Ai by Aj.
Renate A. Schmidt
FM Group |
Last modified: 11 Jul 2000
Copyright © 2000
Renate A. Schmidt,
School of Computer Science, Man Univ, firstname.lastname@example.org