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
Title of the Journal: Journal of Logic and Computation
Publisher Information: Bamberg : Otto-Friedrich-Universität
Year of publication: 2022
Pages: 1-28
Source/Other editions: Journal of Logic and Computation. (2022), S. 1-28. - ISSN: 1465-363X, 0955-792X.
is version of: 10.1093/logcom/exac029
Language(s): English
Licence: Creative Commons - CC BY-SA - Attribution - ShareAlike 4.0 International 
DOI: 10.1093/logcom/exac029
URN: urn:nbn:de:bvb:473-irb-544316
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: Article
Release Date: 20. July 2022

File SizeFormat  
fisba54431.pdf1.43 MBPDFView/Open