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.

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.

We study teams of agents that play against Nature towards achieving a common objective. The agents are assumed to have imperfect information due to partial observability, and have no communication during the play of the game. We propose a natural notion of higher-order knowledge of agents. Based on this notion, we define a class of knowledge-based strategies, and consider the problem of synthesis of strategies of this class. We introduce a multi-agent extension, MKBSC, of the well-known knowledge-based subset construction applied to such games. Its iterative applications turn out to compute higher-order knowledge of the agents. We show how the MKBSC can be used for the design of knowledge-based strategy profiles, and investigate the transfer of existence of such strategies between the original game and in the iterated applications of the MKBSC, under some natural assumptions. We also relate and compare the “intensional” view on knowledge-based strategies based on explicit knowledge representation and update, with the “extensional” view on finite memory strategies based on finite transducers and show that, in a certain sense, these are equivalent.

I consider strategic-form games with transferable utility extended with a phase of negotiations before the actual play of the game, where players can exchange a series of alternating (turn-based) unilaterally binding offers to each other for incentive payments of utilities after the play, conditional only on the recipients playing the strategy indicated in the offer. Every such offer transforms the game payoff matrix by accordingly transferring the offered amount from the offering player's payoff to the recipient's in all outcomes where the indicated strategy is played by the latter. That exchange of offers generates an unbounded-horizon, extensive-form preplay negotiations game, which is the focus of this study. In this paper, I study the case where the players assume that their opponents can terminate the preplay negotiations phase at any stage. Consequently, in their negotiation strategies, the players are guided by myopic rationality reasoning and aim at optimising each of their offers. The main results and findings include a concrete algorithmic procedure for computing players' best offers in the preplay negotiations phase and using it to demonstrate that these negotiations can generally lead to substantial improvement of the payoffs for both players in the transformed game, but they do not always lead to optimal outcomes, as one might expect.

We introduce and study a natural extension of the Alternating time temporal logic ATL, called Temporal Logic of Coalitional Goal Assignments (TLCGA). It features one new and quite expressive coalitional strategic operator, called the coalitional goal assignment operator ⦉ γ ⦊, where γ is a mapping assigning to each set of players in the game its coalitional goal, formalised by a path formula of the language of TLCGA, i.e., a formula prefixed with a temporal operator X, U, or G, representing a temporalised objective for the respective coalition, describing the property of the plays on which that objective is satisfied. Then, the formula ⦉ γ ⦊ intuitively says that there is a strategy profile Σ for the grand coalition Agt such that for each coalition C, the restriction Σ |C of Σ to C is a collective strategy of C that enforces the satisfaction of its objective γ (C) in all outcome plays enabled by Σ |C.

We establish fixpoint characterizations of the temporal goal assignments in a μ-calculus extension of TLCGA, discuss its expressiveness and illustrate it with some examples, prove bisimulation invariance and Hennessy–Milner property for it with respect to a suitably defined notion of bisimulation, construct a sound and complete axiomatic system for TLCGA, and obtain its decidability via finite model property.