Home > Research > Publications & Outputs > A Tableau Calculus for Minimal Modal Model Gene...

Links

Text available via DOI:

View graph of relations

A Tableau Calculus for Minimal Modal Model Generation

Research output: Contribution to Journal/MagazineJournal articlepeer-review

Published
<mark>Journal publication date</mark>3/11/2011
<mark>Journal</mark>Electronic Notes in Theoretical Computer Science
Volume278
Number of pages14
Pages (from-to)159-172
Publication StatusPublished
Early online date29/10/11
<mark>Original language</mark>English

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.