TY - BOOK

T1 - Minimal model reasoning for modal logic

AU - Papacchini, Fabio

PY - 2015

Y1 - 2015

N2 - Model generation and minimal model generation are useful for tasks such as model checking, query answering and for debugging of logical specifications. Due to this variety of applications, several minimality criteria and model generation methods for classical logics have been studied. Minimal model generation for modal logics however did not receive the same attention from the research community.This thesis aims to fill this gap by investigating minimality criteria and designingminimal model generation procedures for all the sublogics of the multi-modal logic S5(m) and their extensions with universal modalities. All the procedures are minimalmodel sound and complete, in the sense that they generate all and only minimal models.The starting point of the investigation is the definition of a Herbrand semantics formodal logics on which a syntactic minimality criterion is devised. The syntactic natureof the minimality criterion allows for an efficient minimal model generation procedure,but, on the other hand, the resulting minimal models can be redundant or semanticallynon minimal with respect to each other.To overcome the syntactic limitations of the first minimality criterion, the thesismoves from minimal modal Herbrand models to semantic minimality criteria based on subset-simulation. At first, theoretical procedures for the generation of models minimal modulo subset-simulation are presented. These procedures for the generation of models minimal modulo subset-simulation are minimal model sound and complete, but they might not terminate. The minimality criterion and the procedures are then refined in such a way that termination can be ensured while preserving minimal model soundness and completeness.

AB - Model generation and minimal model generation are useful for tasks such as model checking, query answering and for debugging of logical specifications. Due to this variety of applications, several minimality criteria and model generation methods for classical logics have been studied. Minimal model generation for modal logics however did not receive the same attention from the research community.This thesis aims to fill this gap by investigating minimality criteria and designingminimal model generation procedures for all the sublogics of the multi-modal logic S5(m) and their extensions with universal modalities. All the procedures are minimalmodel sound and complete, in the sense that they generate all and only minimal models.The starting point of the investigation is the definition of a Herbrand semantics formodal logics on which a syntactic minimality criterion is devised. The syntactic natureof the minimality criterion allows for an efficient minimal model generation procedure,but, on the other hand, the resulting minimal models can be redundant or semanticallynon minimal with respect to each other.To overcome the syntactic limitations of the first minimality criterion, the thesismoves from minimal modal Herbrand models to semantic minimality criteria based on subset-simulation. At first, theoretical procedures for the generation of models minimal modulo subset-simulation are presented. These procedures for the generation of models minimal modulo subset-simulation are minimal model sound and complete, but they might not terminate. The minimality criterion and the procedures are then refined in such a way that termination can be ensured while preserving minimal model soundness and completeness.

UR - http://www.manchester.ac.uk/escholar/uk-ac-man-scw:247065

M3 - Doctoral Thesis

PB - University of Manchester

ER -