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.

For each technical report listed here, copyright and all intellectual property rights remain with the respective authors. Copyright is effective from the year of publication in each case. By downloading a file from this page, you agree to use it only for purposes of research and scholarship. Any other use of this material or storage of it in any medium or its sale or distribution in any form is expressly forbidden without prior written permission from the authors concerned.