Strategies for modal resolution: Results and problems (Q920970)

Automated theorem proving in modal logics, based on resolution, is a challenging problem and has caused some previous erroneous results. The authors suggest the following strategies for propositional modal logic (in fact for the S4 Kripke system): deletion of subsumed clauses, extensions of classical strategies based on a static constraint, negative resolution. A notion of a Horn clause for modal logics is introduced. An implementation of the linear strategy has already been realized. As previous related works we mention that of L. Fariñas and M. Cialdea.