Ordered resolution for coalition logic

U. Hustadt, P. Gainer, C. Dixon, C. Nalon, L. Zhang

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review


In this paper we introduce a calculus based on ordered resolution for Coalition Logic (CL), improving our previous approach based on unrefined resolution, and discuss the problems associated with imposing an ordering refinement in the context of CL. The calculus operates on ‘coalition problems’, a normal form for CL where we use coalition vectors that can represent choices made by agents explicitly, and the inference rules of the calculus provide the basis for a decision procedure for the satisfiability problem in CL. We give correctness, termination and complexity results for our calculus. We also present experimental results for an implementation of the calculus and show that it outperforms a tableau-based decision procedure for Alternating-Time Temporal Logic (CL) on two classes of benchmark formulae for CL.
Original languageEnglish
Title of host publicationAutomated Reasoning with Analytic Tableaux and Related Methods
Subtitle of host publication24th International Conference, TABLEAUX 2015, Wroclaw, Poland, September 21-24, 2015, Proceedings
PublisherSpringer Nature
Number of pages16
ISBN (Electronic)978-3-319-24312-2
ISBN (Print)978-3-319-24311-5
Publication statusPublished - 2015

Publication series

NameLecture Notes in Computer Science
NameLecture Notes in Artificial Intelligence


Dive into the research topics of 'Ordered resolution for coalition logic'. Together they form a unique fingerprint.

Cite this