Tech Reports


Anti-Prenexing and Prenexing for Modal Logics (Extended Version)

Claudia Nalon and Clare Dixon


Efficient proof methods for proving properties specified by means of normal modal logics are highly desirable, as such logical sys- tems have been widely used in computer science to represent complex situations. Resolution-based methods are often designed to deal with for- mulae in a normal form and the efficiency of the method (also) relies on how efficient (in the sense of producing fewer and/or shorter clauses) the translation procedure is. We present a normal form for normal modal logics and show how the use of simplification, for specific normal log- ics, together with anti-prenexing and prenexing techniques help us to produce better sets of clauses.

[Full Paper]