A tableau calculus for minimal modal model generation

Fabio Papacchini, Renate A. Schmidt

    Research output: Contribution to journalArticlepeer-review


    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. © 2011 Elsevier B.V.
    Original languageEnglish
    Pages (from-to)159-172
    Number of pages13
    JournalElectronic Notes in Theoretical Computer Science
    Issue number1
    Publication statusPublished - 3 Nov 2011


    • minimal model generation
    • modal logic
    • model generation
    • tableaux calculus


    Dive into the research topics of 'A tableau calculus for minimal modal model generation'. Together they form a unique fingerprint.

    Cite this