zbMATH — the first resource for mathematics

Realizations and LP. (English) Zbl 1132.03325
Artemov, Sergei N. (ed.) et al., Logical foundations of computer science. International symposium, LFCS 2007, New York, NY, USA, June 4–7, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-72732-3/pbk). Lecture Notes in Computer Science 4514, 212-223 (2007).
Summary: LP can be seen as a logic of knowledge with justifications. Artemov’s Realization Theorem says justifications can be extracted from validities in the Hintikka-style logic of knowledge S4, where they are not explicitly present. We provide tools for reasoning about justifications directly. Among other things, we provide machinery for combining two realizations of the same formula, and for replacing subformulas by equivalent subformulas. The results are algorithmic in nature-semantics for LP plays no role. We apply our results to provide a new algorithmic proof of Artemov’s Realization Theorem itself.
For the entire collection see [Zbl 1121.03005].

03B45 Modal logic (including the logic of norms)
03B42 Logics of knowledge and belief (including belief change)
03F45 Provability logics and related algebras (e.g., diagonalizable algebras)
logic of proofs
Full Text: DOI