-
Automating Public Announcement Logic with Relativized Common Knowledge as a Fragment of HOL in LogiKEy
Authors:
Christoph Benzmüller,
Sebastian Reiche
Abstract:
A shallow semantical embedding for public announcement logic with relativized common knowledge is presented. This embedding enables the first-time automation of this logic with off-the-shelf theorem provers for classical higher-order logic. It is demonstrated (i) how meta-theoretical studies can be automated this way, and (ii) how non-trivial reasoning in the target logic (public announcement logi…
▽ More
A shallow semantical embedding for public announcement logic with relativized common knowledge is presented. This embedding enables the first-time automation of this logic with off-the-shelf theorem provers for classical higher-order logic. It is demonstrated (i) how meta-theoretical studies can be automated this way, and (ii) how non-trivial reasoning in the target logic (public announcement logic), required e.g. to obtain a convincing encoding and automation of the wise men puzzle, can be realized.
Key to the presented semantical embedding is that evaluation domains are modeled explicitly and treated as an additional parameter in the encodings of the constituents of the embedded target logic; in previous related works, e.g. on the embedding of normal modal logics, evaluation domains were implicitly shared between meta-logic and target logic.
The work presented in this article constitutes an important addition to the pluralist LogiKEy knowledge engineering methodology, which enables experimentation with logics and their combinations, with general and domain knowledge, and with concrete use cases -- all at the same time.
△ Less
Submitted 27 January, 2022; v1 submitted 2 November, 2021;
originally announced November 2021.
-
Public Announcement Logic in HOL
Authors:
Sebastian Reiche,
Christoph Benzmüller
Abstract:
A shallow semantical embedding for public announcement logic with relativized common knowledge is presented. This embedding enables the first-time automation of this logic with off-the-shelf theorem provers for classical higher-order logic. It is demonstrated (i) how meta-theoretical studies can be automated this way, and (ii) how non-trivial reasoning in the target logic (public announcement logi…
▽ More
A shallow semantical embedding for public announcement logic with relativized common knowledge is presented. This embedding enables the first-time automation of this logic with off-the-shelf theorem provers for classical higher-order logic. It is demonstrated (i) how meta-theoretical studies can be automated this way, and (ii) how non-trivial reasoning in the target logic (public announcement logic), required e.g. to obtain a convincing encoding and automation of the wise men puzzle, can be realized. Key to the presented semantical embedding -- in contrast, e.g., to related work on the semantical embedding of normal modal logics -- is that evaluation domains are modeled explicitly and treated as additional parameter in the encodings of the constituents of the embedded target logic, while they were previously implicitly shared between meta logic and target logic.
△ Less
Submitted 2 October, 2020;
originally announced October 2020.
-
Perfect Prediction Equilibrium
Authors:
Ghislain Fourny,
Stéphane Reiche,
Jean-Pierre Dupuy
Abstract:
In the framework of finite games in extensive form with perfect information and strict preferences, this paper introduces a new equilibrium concept: the Perfect Prediction Equilibrium (PPE).
In the Nash paradigm, rational players consider that the opponent's strategy is fixed while maximizing their payoff. The PPE, on the other hand, models the behavior of agents with an alternate form of ration…
▽ More
In the framework of finite games in extensive form with perfect information and strict preferences, this paper introduces a new equilibrium concept: the Perfect Prediction Equilibrium (PPE).
In the Nash paradigm, rational players consider that the opponent's strategy is fixed while maximizing their payoff. The PPE, on the other hand, models the behavior of agents with an alternate form of rationality that involves a Stackelberg competition with the past.
Agents with this form of rationality integrate in their reasoning that they have such accurate logical and predictive skills, that the world is fully transparent: all players share the same knowledge and know as much as an omniscient external observer. In particular, there is common knowledge of the solution of the game including the reached outcome and the thought process leading to it. The PPE is stable given each player's knowledge of its actual outcome and uses no assumptions at unreached nodes.
This paper gives the general definition and construction of the PPE as a fixpoint problem, proves its existence, uniqueness and Pareto optimality, and presents two algorithms to compute it. Finally, the PPE is put in perspective with existing literature (Newcomb's Problem, Superrationality, Nash Equilibrium, Subgame Perfect Equilibrium, Backward Induction Paradox, Forward Induction).
△ Less
Submitted 29 January, 2021; v1 submitted 22 September, 2014;
originally announced September 2014.
