Destructive Modal Resolution
- 1 July 1990
- journal article
- Published by Oxford University Press (OUP) in Journal of Logic and Computation
- Vol. 1 (1) , 83-97
- https://doi.org/10.1093/logcom/1.1.83
Abstract
We present non-clausal resolution systems for prepositional modal logics whose Kripke models do not involve symmetry, and for first-order versions whose Kripke models do not involve constant domains. We given systems for K, T, K4, and S4; other logics are also possible. Our systems do not require preliminary reduction to a normal form and, in the first-order case, intermingle resolution steps with Skolemization steps.Keywords
This publication has 0 references indexed in Scilit: