@inproceedings{27eff5a79a1a4cb3afa0499cc7baeffd,

title = "Model Construction for Modal Clauses",

abstract = "We present deterministic model construction algorithms for sets of modal clauses saturated with respect to three refinements of the modal-layered resolution calculus implemented in the prover KSP. The model construction algorithms are inspired by the Bachmair-Ganzinger method for constructing a model for a set of ground first-order clauses saturated with respect to ordered resolution with selection. The challenge is that the inference rules of the modal-layered resolution calculus for modal operators are more restrictive than an adaptation of ordered resolution with selection for these would be. While these model construction algorithms provide an alternative means to proving completeness of the calculus, our main interest is the provision of a {\textquoteleft}certificate{\textquoteright} for satisfiable modal formulae that can be independently checked to assure a user that the result of KSP is correct. This complements the existing provision of proofs for unsatisfiable modal formulae.",

author = "Ullrich Hustadt and Fabio Papacchini and Cl{\'a}udia Nalon and Clare Dixon",

year = "2024",

month = jul,

day = "2",

doi = "10.1007/978-3-031-63501-4_1",

language = "English",

isbn = "978-3-031-63500-7",

series = "Automated Reasoning",

publisher = "Springer Nature",

pages = "3--23",

booktitle = "International Joint Conference on Automated Reasoning 2024",

address = "United States",

}