Automating Public Announcement Logic with Relativized Common Knowledge as a Fragment of HOL in LogiKEy

Faculty/Professorship: AI Systems Engineering 
Author(s): Benzmüller, Christoph  ; Reiche, Sebastian
Publisher Information: Bamberg : Otto-Friedrich-Universität
Year of publication: 2022
Pages: 1-28
Source/Other editions: arXiv (Online). 2021. - DOI: 10.48550/ARXIV.2111.01654.
is version of: 10.48550/ARXIV.2111.01654
Year of first publication: 2021
Language(s): English
Später erschienen in:
Journal of Logic and Computation. (2022), S. 1-28
DOI: 10.1093/logcom/exac029.
Licence: German Act on Copyright 
URN: urn:nbn:de:bvb:473-irb-555593
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.
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: 004 Computer science  
510 Mathematics  
RVK Classification: SK 130   
Type: Preprint
Release Date: 19. September 2022

File SizeFormat  
fisba55559.pdf1.41 MBPDFView/Open