论文标题
HOL中的公告逻辑
Public Announcement Logic in HOL
论文作者
论文摘要
提出了具有相对常识的公共公告逻辑的浅色语义嵌入。这种嵌入使该逻辑的首次自动化具有用于经典高阶逻辑的现成定理鉴定。它证明了（i）如何以这种方式自动化元理论研究，以及（ii）目标逻辑中的非平凡推理（公开公告逻辑）是如何所需的，例如为了获得令人信服的编码和自动化，智者难题可以实现。相反，在正常模态逻辑的语义嵌入的相关工作中，所提出的语义嵌入的关键是，在嵌入式目标逻辑的组成部分的编码中，对评估域进行了显式建模并将其视为附加参数，而这些参数先前是在MetA Logic和Target Logic之间共享的。
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 -- in contrast, e.g., to related work on the semantical embedding of normal modal logics -- is that evaluation domains are modeled explicitly and treated as additional parameter in the encodings of the constituents of the embedded target logic, while they were previously implicitly shared between meta logic and target logic.
