Complete axiomatization and decidability of the logic of two-agent cooperative strategic interaction

The multi-agent Socially Friendly Coalition Logic SFCL was introduced in [1]. The present paper focuses on the two-agent fragment SFCL ( 2 ) of SFCL . We illustrate the use of SFCL ( 2 ) for formalising reasoning about two-agent interaction enabling cooperative strategic behaviour. Then we prove completeness of an axiomatic system for the 2-agent case SFCL ( 2 ) essentially extracted from the one for SFCL presented in [1] . The proof method is fully constructive and produces finite tree-like models for all consistent SFCL ( 2 ) -formulae, thus also implying decidability of that logic. The proof method is, in principle, generically extendable to the full SFCL and to various other logics for local strategic reasoning.