Description logic for coalitions
İnanç Seylan, Wojciech Jamroga · 2009
Coalition Logic (CL) is one of the most important formalisms for specification and verification of game-like multi-agent systems. Several extensions of the logic have been studied in the literature. These extensions are usually fusions (independent joins) of CL with other modal logics (e.g., temporal, epistemic, dynamic, etc.), and they are generally propositional. In this paper, we propose a game description logic called CLALC which is based on a product of Coalition Logic with the description logic ALC. The new logic allows one to reason about agents' ability to influence first-order structures. We show that the satisfiability problem for CLALC is decidable; we prove this by giving a goal-directed decision procedure for the problem.