Tractable transformations from modal provability logics into first-order logic
This work, consisting of six parts and an appendix, deals with modal provability logics, display calculi and transformations from LF into L. The main result of the paper is Theorem 5. The statements below are equivalent: 1. For all formulae \( \phi, \phi \in \text{LF} \) iff \( f(\phi,1) \in \text{L}\). 2. LF is pseudo displayable. Let K be the standard axiomatic Hilbert system and let L be an extension of K (including K). In the second part the following well-known extensions L of K: T, K4, S4, G, Grz are considered. (For the logics K4, KD4 and S4 the transformation approach is based on a resolution decision procedure considered by \textit{H. Ganzinger, U. Hustadt, C. Mayer} and \textit{R. Schmidt} [in: Advances in modal logic '98, AiML'98 (Uppsala University, Uppsala), 182-191 (1998)]. Let L be any proper displayable logic and let F be any formula generation map. The authors write LF to denote the logic obtained from L by addition of the scheme \( \square (F(p) \Rightarrow p) \Rightarrow \square p \). In part three the authors define the calculus \(\delta \text{LF}\). They say that LF is pseudo displayable iff for any \(\phi \in \text{FML}\), \(I \vdash \phi \) has a proof in \(\delta \text{LF}\) iff \( I \vdash \phi \) has a cut-free proof in \(\delta \text{LF}\). Then, using Belnap's proof-theoretical framework Display Logic [\textit{N. D. Belnap}, J. Philos. Logic 11, 375-417 (1982; Zbl 0509.03008)], the authors characterize the ``pseudo-displayable subclass of LF and show how to define polynomial-time transformations from each such LF into the corresponding L, and hence into first-order classical logic. In most cases the proofs of the authors' results are omitted. For the entire collection see [Zbl 0917.00015].
- Tableau-based translation from first-order logic to modal logic
- Implementing and evaluating provers for first-order modal logics
- A proof theoretic tool for first-order modal logic
- On the proof-theory of two formalisations of modal first-order logic
- Modal Logics Between Propositional and First-order
- scientific article; zbMATH DE number 4037817
- scientific article; zbMATH DE number 3924750
- HOL Based First-Order Modal Logic Provers
- Alternative translation techniques for propositional and first-order modal logics
- A modal provability logic of explicit and implicit proofs
This page was built for publication: Tractable transformations from modal provability logics into first-order logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4263154)
