A Tableau Calculus for Minimal Modal Model Generation

• DOI: 10.1016/j.entcs.2011.10.013
• Publication Date: 2011-10-31T08:30:59Z
• Authors: Fabio Papacchini; Renate A. Schmidt
• Keywords: model generation; 0102 computer and information sciences; minimal model generation; 01 natural sciences; 004; tableaux calculus; modal logic; Theoretical Computer Science; Computer Science(all)

AbstractModel 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.