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

This paper proposes and studies a mechanism modelling the emergence of cooperation in non-cooperative multi-player extensive form games. We consider such games enriched with additional “stage bidding actions”, where at each decision node of the game tree, before the player controlling that node makes a decision every other player may make a committed offer (‘bid’) to pay an explicitly proposed amount of utility to the controlling player if she makes the choice explicitly indicated in the bid. In this work we assume that the bids are made simultaneously by all players. The controlling player then considers all these bids and then decides on its move. The effect of each bid associated with that choice is that it modifies the payoffs in the respective subgame according to the bid by transferring the proposed amounts of utility from the bidder to the controlling player who made the choice; all other bids made at that stage become irrelevant. Thus, these stage bids serve as an incentives-based mechanism that enables reaching a mutually beneficial cooperation in extensive form games.We study the resulting multi-player extensive form games with incentive bidding, which we call incentive bidding games (IB games), and analyze the subgame perfect equilibria (SPE) in these games. We show constructively that all IB games have (possibly many) SPE, and that the SPE outcomes (i.e. payoff tuples) form a polytope in the space of all outcomes. In the case of 2-player games, we also prove for an arbitrary game tree that all the SPE are sum-maximizing and have the same outcome, thereby defining a unique “value” of the game. These results contrast some well-known drawbacks of SPE in standard extensive form games and provide a further strong motivation for studying extensive form games with incentive bidding.We also study the notion of strong SPE in the sense of Aumann for IB games. First, we show that each of these strong SPE maximizes the sum of the payoffs (thus achieving a socially optimal solution). Second, if the game tree is binary, the strong SPE outcomes form a convex polytope. Third, games with only two leaves have such strong SPE, and we conjecture that all games with binary decision trees and with the same controlling player at all decision nodes have, indeed, such strong SPE.

This paper is a follow-up to our recent work, where we apply and extend the theory and methods of algorithmic correspondence theory previously developed for modal logics to the language ℒR of relevance logics with respect to their standard Routley-Meyer relational semantics. In the above mentioned precursor of the present work we develop a non-deterministic algorithmic procedure PEARL for computing first-order equivalents in terms of that semantics and proving canonicity of formulae of a language ℒR+ extending ℒR with all residuals and adjoints of the connectives in ℒR. We identified a large syntactically defined class of inductive formulae in ℒR, and showed that PEARL succeeds for every so defined inductive formula. In this work we present an alternative approach to defining inductive formulae for relevance logics, originally developed for polyadic modal logics in earlier works by Goranko and Vakarelov, based on a rewriting of the language ℒR that allows composing logical connectives into composite ‘box’ and ‘diamond’ terms that enable a ‘flat’ representation of formulae of ℒR, thus providing a technically simplified definition of the class of inductive formulae. We show that, modulo translation, the two approaches define the same class of inductive formulae, and explain how PEARL can be modified to work on ‘flat’ inductive formulae.

This is the first paper in a series exploring the following generic question for a given type of combination of logics: Given tableaux systems for two logics and a combination of these logics of a given type, how to combine systematically and uniformly the tableaux systems for component logics into a tableaux system for the combined logic by preserving important properties of the components? Here I consider the case of general fibring of logics, introduced by Dov Gab-bay. Starting with the basic cases of propositional merger and simple nesting of logics, I present natural generic versions of fibring of tableaux for these constructions, illustrate them with some examples, and establish respective results on preservation of soundness, completeness, and termination from the component tableaux to the combined tableau. Then I extend the combined tableau construction to the general case of fibring by iterating the basic cases and mention some potential applications.

Trees are partial orders in which every element has a linearly ordered set of predecessors. Here we initiate the exploration of the structural theory of trees with the study of different notions of branching in trees and of condensed trees, which are trees in which every node is a branching node. We then introduce and investigate two different constructions of tree condensations-one shrinking, and the other expanding, the tree to a condensed tree.

Trees are partial orderings where every element has a linearly ordered set of smaller elements. We define and study several natural notions of completeness of trees, extending Dedekind completeness of linear orders and Dedekind-MacNeille completions of partial orders. We then define constructions of tree completions that extend any tree to a minimal one satisfying the respective completeness property.

Temporal Logics are a rich variety of logical systems designed for formalising reasoning about time, and about events and changes in the world over time. These systems differ by the ontological assumptions made about the nature of time in the associated models, by the logical languages involving various operators for composing temporalized expressions, and by the formal logical semantics adopted for capturing the precise intended meaning of these temporal operators. Temporal logics have found a wide range of applications as formal frameworks for temporal knowledge representation and reasoning in artificial intelligence, and as tools for formal specification, analysis, and verification of properties of computer programs and systems. This Element aims at providing both a panoramic view on the landscape of the variety of temporal logics and closer looks at some of their most interesting and important landmarks. 

We consider systems of rational agents who act and interact in pursuit of their individual and collective objectives. We study and formalise the reasoning of an agent, or of an external observer, about the expected choices of action of the other agents based on their objectives, in order to assess the reasoner’s ability, or expectation, to achieve their own objective. To formalize such reasoning we extend Pauly’s Coalition Logic with three new modal operators of conditional strategic reasoning, thus introducing the Logic for Local Conditional Strategic Reasoning ConStR. We provide formal semantics for the new conditional strategic operators in concurrent game models, introduce the matching notion of bisimulation for each of them, prove bisimulation invariance and Hennessy–Milner property for each of them, and discuss and compare briefly their expressiveness. Finally, we also propose systems of axioms for each of the basic operators of ConStR and for the full logic.

We apply and extend the theory and methods of algorithmic correspondence theory for modal logics, developed over the past 20 years, to the language L_R of relevance logics with respect to their standard Routley–Meyer relational semantics. We develop the non-deterministic algorithmic procedure PEARLPEARL for computing first-order equivalents of formulae of the language L_R, in terms of that semantics. PEARLPEARL is an adaptation of the previously developed algorithmic procedures SQEMA (for normal modal logics) and ALBA (for distributive and non-distributive modal logics). We then identify a large syntactically defined class of inductive formulae in L_R, analogous to previously defined such classes in the classical, distributive and non-distributive modal logic settings, and show that PEARLPEARL succeeds for every inductive formula and correctly computes a first-order definable condition which is equivalent to it with respect to frame validity. We also provide a detailed comparison with two earlier works, each extending the class of Sahlqvist formulae to relevance logics, and show that both are subsumed by simple subclasses of inductive formulae.

We propose a general framework for modelling and formal reasoning about multi-agent systems and, in particular, multi-stage games where both quantitative and qualitative objectives and constraints are involved. Our models enrich concurrent game models with payoffs and guards on actions associated with each state of the model and propose a quantitative extension of the logic ATL* that enables the combination of quantitative and qualitative reasoning. We illustrate the framework with some detailed examples. Finally, we consider the model-checking problems arising in our framework and establish some general undecidability and decidability results for them.