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

Research

Associated organisational unit

Links

Text available via DOI:

Keywords

View graph of relations

A Tableau Calculus for Minimal Modal Model Generation

Research output: Contribution to Journal/Magazine › Journal article › peer-review

Published

Standard

A Tableau Calculus for Minimal Modal Model Generation. / Papacchini, Fabio; Schmidt, Renate A.
In: Electronic Notes in Theoretical Computer Science, Vol. 278, 03.11.2011, p. 159-172.

Research output: Contribution to Journal/Magazine › Journal article › peer-review

Harvard

Papacchini, F & Schmidt, RA 2011, 'A Tableau Calculus for Minimal Modal Model Generation', Electronic Notes in Theoretical Computer Science, vol. 278, pp. 159-172. https://doi.org/10.1016/j.entcs.2011.10.013

APA

Papacchini, F., & Schmidt, R. A. (2011). A Tableau Calculus for Minimal Modal Model Generation. Electronic Notes in Theoretical Computer Science, 278, 159-172. https://doi.org/10.1016/j.entcs.2011.10.013

Vancouver

Papacchini F, Schmidt RA. A Tableau Calculus for Minimal Modal Model Generation. Electronic Notes in Theoretical Computer Science. 2011 Nov 3;278:159-172. Epub 2011 Oct 29. doi: 10.1016/j.entcs.2011.10.013

Author

Papacchini, Fabio ; Schmidt, Renate A. / A Tableau Calculus for Minimal Modal Model Generation. In: Electronic Notes in Theoretical Computer Science. 2011 ; Vol. 278. pp. 159-172.

Bibtex

@article{5fe5fc2447f344fb95e758d0178a5b86,
title = "A Tableau Calculus for Minimal Modal Model Generation",
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.",
keywords = "tableaux calculus, modal logic, minimal model generation, model generation",
author = "Fabio Papacchini and Schmidt, {Renate A.}",
year = "2011",
month = nov,
day = "3",
doi = "10.1016/j.entcs.2011.10.013",
language = "English",
volume = "278",
pages = "159--172",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",

}

RIS

TY - JOUR

T1 - A Tableau Calculus for Minimal Modal Model Generation

AU - Papacchini, Fabio

AU - Schmidt, Renate A.

PY - 2011/11/3

Y1 - 2011/11/3

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

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

KW - tableaux calculus

KW - modal logic

KW - minimal model generation

KW - model generation

U2 - 10.1016/j.entcs.2011.10.013

DO - 10.1016/j.entcs.2011.10.013

M3 - Journal article

VL - 278

SP - 159

EP - 172

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -