Search

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.

The paper deals with multiplayer normal form games which are preceded by a ‘preplay negotiation phase’ consisting of exchange of preplay offers by players for payments of utility to other players conditional on them playing designated in the offers strategies. The game-theoretic effect of such preplay offers is a transformation of the payoff matrix of the game, obtained by transferring the offered payments between the payoffs of the respective players; thus, certain groups of game matrix transformations naturally emerge. The main result is an explicit and rather transparent algebraic characterization of the possible transformations of the payoff matrix of any given N-person normal form game induced by preplay offers for transfer of payments. That result can be used to describe the ‘bargaining space’ of the game and to determine the mutually optimal game transformations that rational players can achieve by exchange of preplay offers.

Hybrid deduction–refutation systems are deductive systems intended to derive both valid and non-valid, i.e., semantically refutable, formulae of a given logical system, by employing together separate derivability operators for each of these and combining ‘hybrid derivation rules’ that involve both deduction and refutation. The goal of this paper is to develop a basic theory and ‘meta-proof’ theory of hybrid deduction–refutation systems. I then illustrate the concept on a hybrid derivation system of natural deduction for classical propositional logic, for which I show soundness and completeness for both deductions and refutations.

We propose a logical framework combining a game-theoretic study of abilities of agents to achieve quantitative objectives in multi-player games by optimizing payoffs or preferences on outcomes with a logical analysis of the abilities of players for achieving qualitative objectives of players, i.e., reaching or maintaining game states with desired properties. We enrich concurrent game models with payoffs for the normal form games associated with the states of the model and propose a quantitative extension of the logic ATL* enabling the combination of quantitative and qualitative reasoning.

Modal formulae express monadic second-order properties on Kripke frames, but in many important cases these have first-order equivalents. Computing such equivalents is important for both logical and computational reasons. On the other hand, canonicity of modal formulae is important, too, because it implies frame-completeness of logics axiomatized with canonical formulae. Computing a first-order equivalent of a modal formula amounts to elimination of second-order quantifiers. Two algorithms have been developed for second-order quantifier elimination: SCAN, based on constraint resolution, and DLS, based on a logical equivalence established by Ackermann. In this paper we introduce a new algorithm, SQEMA, for computing first-order equivalents (using a modal version of Ackermann's lemma) and, moreover, for proving canonicity of modal formulae. Unlike SCAN and DLS, it works directly on modal formulae, thus avoiding Skolemization and the subsequent problem of unskolemization. We present the core algorithm and illustrate it with some examples. We then prove its correctness and the canonicity of all formulae on which the algorithm succeeds. We show that it succeeds not only on all Sahlqvist formulae, but also on the larger class of inductive formulae, introduced in our earlier papers. Thus, we develop a purely algorithmic approach to proving canonical completeness in modal logic and, in particular, establish one of the most general completeness results in modal logic so far.