@ARTICLE{Schmidt08b,
AUTHOR = {Schmidt, R. A.},
YEAR = {2009},
TITLE = {A New Methodology for Developing Deduction Methods},
JOURNAL =  {Annals of Mathematics and Artificial Intelligence},
VOLUME = {55},
NUMBER = {1--2},
PAGES = {155--187},
URL = {http://dx.doi.org/10.1007/s10472-009-9155-4},
ABSTRACT = {This paper explores the use of resolution as a meta-framework 
for developing various, different deduction calculi.  In this work the 
focus is on developing deduction calculi for modal dynamic logics.  
Dynamic modal logics are PDL-like extended modal logics which are closely 
related to description logics.  We show how tableau systems, modal 
resolution systems and Rasiowa-Sikorski systems can be developed and 
studied by using standard principles and methods of first-order theorem 
proving.  The approach is based on the translation of reasoning problems 
in modal logic to first-order clausal form and using a suitable refinement 
of resolution to construct and mimic derivations of the desired proof 
method. The inference rules of the calculus can then be read off from the 
clausal form. We show how this approach can be used to generate new proof 
calculi and prove soundness, completeness and decidability results. This 
slightly unusual approach allows us to gain new insights and results for 
familiar and less familiar logics, for different proof methods, and 
compare them not only theoretically but also empirically in a uniform 
framework.
}
}