A resolution-based calculus for Coalition Logic


Nalon, Cláudia, Zhang, Lan, Dixon, Clare ORCID: 0000-0002-4610-9533 and Hustadt, Ullrich ORCID: 0000-0002-0455-0267 (2014) A resolution-based calculus for Coalition Logic. Journal of Logic and Computation, 24 (4). pp. 883-917.

[img] Text (Accepted version)
NZDH-CL-resolution-jlc-2013-10-19.pdf - Author Accepted Manuscript
Download (508kB)

Abstract

We present a resolution-based calculus for Coalition Logic CL, a non-normal modal logic used for reasoning about cooperative agency. We introduce a normal form and a set of inference rules to solve the satisfiability problem in CL. We also show that the calculus presented here is sound, complete, and terminating.

Item Type: Article
Additional Information: First published online: January 21, 2014. Issue date: August 2014. Cited as: Cláudia Nalon, Lan Zhang, Clare Dixon, and Ullrich Hustadt A resolution-based calculus for Coalition Logic J Logic Computation first published online January 21, 2014 doi:10.1093/logcom/ext074
Uncontrolled Keywords: Coalition Logic, Theorem-Proving, Resolution Method
Subjects: ?? QA75 ??
Divisions: Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science
Depositing User: Symplectic Admin
Date Deposited: 29 Apr 2014 15:19
Last Modified: 16 Dec 2022 04:41
DOI: 10.1093/logcom/ext074
Publisher's Statement : This is a pre-copyedited, author-produced PDF of an article accepted for publication in Journal of Logic and Computation following peer review. The version of recordCláudia Nalon, Lan Zhang, Clare Dixon, and Ullrich Hustadt A resolution-based calculus for Coalition Logic J Logic Computation first published online January 21, 2014 doi:10.1093/logcom/ext074 is available online at: http://doi.org/10.1093/logcom/ext074
Related URLs:
URI: https://livrepository.liverpool.ac.uk/id/eprint/15113
Dimensions
Altmetric
CORE (COnnecting REpositories)