{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T13:21:46Z","timestamp":1758979306351},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>The aim of this work is to define a resolution method for the modal logic S5. We<\/jats:p><jats:p>first propose a conjunctive normal form (S5-CNF) which is mainly based on using labels<\/jats:p><jats:p>referring to semantic worlds. In a sense, S5-CNF can be seen as a generalization of the<\/jats:p><jats:p>conjunctive normal form in propositional logic by using in the clause structure the modal<\/jats:p><jats:p>connective of necessity and labels. We show that every S5 formula can be transformed<\/jats:p><jats:p>into an S5-CNF formula using a linear encoding. Then, in order to show the suitability<\/jats:p><jats:p>of our normal form, we describe a modeling of the problem of graph coloring. Finally, we<\/jats:p><jats:p>introduce a simple resolution method for S5, composed of three deductive rules, and we<\/jats:p><jats:p>show that it is sound and complete. Our deductive rules can be seen as adaptations of<\/jats:p><jats:p>Robinson\u2019s resolution rule to the possible-worlds semantics.<\/jats:p>","DOI":"10.29007\/1zgr","type":"proceedings-article","created":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T18:04:14Z","timestamp":1516730654000},"page":"252-240","source":"Crossref","is-referenced-by-count":1,"title":["A Resolution Method for Modal Logic S5"],"prefix":"10.29007","volume":"36","author":[{"given":"Yakoub","family":"Salhi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Sioutis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"11545","event":{"name":"GCAI 2015. Global Conference on Artificial Intelligence"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T18:04:21Z","timestamp":1516730661000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/easychair.org\/publications\/paper\/3XXQ"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.29007\/1zgr","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}