@TECHREPORT{SchmidtHustadt03a,
AUTHOR = {Schmidt, R. A. and Hustadt, U.},
MONTH = {January},
YEAR = {2003},
TITLE = {Mechanised Reasoning and Model Generation for Extended Modal Logics},
TYPE = {Preprint Series},
NUMBER = {CSPP-19},
INSTITUTION = {University of Manchester},
ADDRESS = {UK},
NOTE = {Submitted for publication.} ,
URL = {\url{http://www.cs.man.ac.uk/~schmidt/publications/SchmidtHustadt03a.html}},
ABSTRACT = {
The approach presented in this overview paper exploits that
modal logics can be seen to be fragments of first-order logic and
deductive methods can be developed and studied within the framework
of first-order resolution.
We focus on a class of extended modal logics very similar in spirit to
propositional dynamic logic and closely related to description logics.
We review and discuss the development of decision procedures
for decidable extended modal logics and look at methods for
automatically generating models.
}
}