Options
Automating Public Announcement Logic with Relativized Common Knowledge as a Fragment of HOL in LogiKEy
Benzmüller, Christoph; Reiche, Sebastian (2021): „Automating Public Announcement Logic with Relativized Common Knowledge as a Fragment of HOL in LogiKEy“. Online: arXiv doi: 10.48550/ARXIV.2111.01654.
Author:
Publisher Information:
Year of publication:
2021
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:
Preprint
Activation date:
September 19, 2022
Versioning
Question on publication
Permalink
https://fis.uni-bamberg.de/handle/uniba/55605