# Tech Reports

## ULCS-06-003

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

Claudia Nalon and Clare Dixon

### Abstract

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]