© 1990 by Oxford University Press
Original Articles |
Destructive Modal Resolution1
Department of Mathematics and Computer Science, Lehman College (CUNY) Bronx, NY 1046
Departments of Computer Science, Philosophy, Mathematics, Graduate Center (CUNY), 33 West 42nd Street, NYC, NY 100362
2 Research partly supported by NSF Grant CCR-8702307 and PSC-CUNY Grant 667295
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.