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 ![]() |
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: | German Act on Copyright |
DOI: | 10.1093/logcom/exac029 |
URN: | urn:nbn:de:bvb:473-irb-544316 |
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. |
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 |
URI: | https://fis.uni-bamberg.de/handle/uniba/54431 |
Release Date: | 20. July 2022 |
File | Size | Format | |
---|---|---|---|
fisba54431.pdf | 1.41 MB | View/Open |

originated at the
University of Bamberg
University of Bamberg