Options
Automating public announcement logic with relativized common knowledge as a fragment of HOL in LogiKEy
Benzmüller, Christoph; Reiche, Sebastian (2023): „Automating public announcement logic with relativized common knowledge as a fragment of HOL in LogiKEy“. Eynsham, Oxford: Oxford Univ. Press doi: 10.1093/logcom/exac029.
Author:
Title of the Journal:
Journal of Logic and Computation
ISSN:
1465-363X
0955-792X
Publisher Information:
Year of publication:
2023
Volume:
33
Issue:
6
Pages:
Language:
English
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 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 mod- eled explicitly and treated as an additional parameter in the encodings of the con- stituents of the embedded target logic; in previous related works, e.g. on the em- bedding 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 experimen- tation with logics and their combinations, with general and domain knowledge, and with concrete use cases — all at the same time.
Key to the presented semantical embedding is that evaluation domains are mod- eled explicitly and treated as an additional parameter in the encodings of the con- stituents of the embedded target logic; in previous related works, e.g. on the em- bedding 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 experimen- tation with logics and their combinations, with general and domain knowledge, and with concrete use cases — all at the same time.
GND Keywords: ; ; ; ; ;
Mathematische Logik
Ankündigung
Allgemeinwissen
Semantik
HOL
Automatisches Beweisverfahren
Keywords:
Public announcement logic; Relativized common knowledge; Semantical embedding; Higher-order logic; Proof automation
DDC Classification:
RVK Classification:
Type:
Article
Activation date:
July 8, 2022
Versioning
Question on publication
Permalink
https://fis.uni-bamberg.de/handle/uniba/54497