@ARTICLE{PapacchiniSchmidt11,
AUTHOR = {Papaccini, F. and Schmidt, R. A.},
YEAR = {2011},
TITLE = {A Tableau Calculus for Minimal Modal Model Generation},
JOURNAL = {Electronic Notes in Theoretical Computer Science},
VOLUME = {278},
NUMBER = {3},
PAGES = {159--172},
ABSTRACT = {
Model generation and minimal model generation is useful for fault analysis,
verification of systems and validation of data models. Whereas for classical
propositional and first-order logic several model minimization approaches
have been developed and studied, for non-classical logic the topic has been
much less studied. In this paper we introduce a minimal model generation calculus
for multi-modal logic K(m) and extensions of K(m) with the axioms T and B. 
The calculus provides a method to generate all and only minimal modal Herbrand 
models, and each model is generated exactly once. A novelty of the calculus is 
a non-standard complement splitting rule designed for minimal model generation. 
Experiments show the rule has the added benefit of reducing the search space.
}
}