Unification in pretabular extensions of S4
The paper is dedicated to the study of pretabular extensions of modal logic \(\mathrm{S4}\) described in [\textit{L. L. Maksimova}, Algebra Logic 14, 16--33 (1976; Zbl 0319.02019); translation from Algebra Logika 14, 28--55 (1975)]: \[ \begin{array}{l} \mathrm{PM1 := S}4.3 + \mathcal{G}rz,\\ \mathrm{PM2} := \mathcal{G}rz + \sigma_2,\\ \mathrm{PM3} := \mathcal{G}rz + [\Box r \lor \Box(\Box r \to \sigma_2)] + (\Box\Diamond p \Leftrightarrow \Diamond\Box p),\\ \mathrm{PM4 := S}4 +[\Box p \lor \Box (\Box p \to \Box q \lor \Box \Diamond \neg q)] + (\Box \Diamond p \leftrightarrow \Diamond\Box p),\\ \mathrm{PM5 := S}5, \end{array} \] where \(\mathcal{G}rz := [\Box(\Box(p \to \Box p) \to p) \to p]\)\\ and \(\sigma_2 := [\Box p \lor \Box (\Box p \to \Box q \lor \Box \Diamond \neg q)]\). It is proven that the logics \(\mathrm{PM2}\) and \(\mathrm{PM3}\) have a finitary unification type, while the logics \(\mathrm{PM1, PM4}\) and \(\mathrm{PM5}\) have a unitary unification type, and any unifiable in \(\mathrm{PM1, PM4}\) or \(\mathrm{PM5}\) formula is projective.
- A criterion for admissibility of rules in the modal system S4 and intuitionistic logic
- A Machine-Oriented Logic Based on the Resolution Principle
- A syntactic approach to unification in transitive reflexive modal logics
- Admissibility of logical inference rules
- Bases of admissible inference rules in tabular modal logics of depth 2
- Best solving modal equations
- Best unifiers in transitive modal logics
- Blending margins: the modal logic K has nullary unification type
- Computer Science Logic
- Decidability of the admissibility problem in layer-finite logics
- Discriminator varieties and symbolic computation
- Extensions of the Lewis system S5
- Five critical modal systems
- scientific article; zbMATH DE number 2015264 (Why is no real title available?)
- Independent bases for admissible rules of pretabular modal logic and its extensions
- LC and its pretabular relatives
- On the admissible rules of intuitionistic propositional logic
- Pretabular extensions of Lewis S4
- Projective formulas and unification in linear discrete temporal multi-agent logics
- Projective unification in modal logic
- Remarks on projective unifiers
- Unification in Linear Modal Logic on Non-transitive Time with the Universal Modality
- Unification in modal and description logics
- Unification theory
- Unification through projectivity
- Modal consequence relations extending S4.3: an application of projective unification
- scientific article; zbMATH DE number 1189062 (Why is no real title available?)
- scientific article; zbMATH DE number 2015264 (Why is no real title available?)
- Inference rules with metavariables and logical equations in the pretabular modal logic PM1
- Unification and Finite Model Property for Linear Step-Like Temporal Multi-Agent Logic with the Universal Modality
- Linear step-like logic of knowledge \(\mathcal{LTK}.{sl} \)
This page was built for publication: Unification in pretabular extensions of S4
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2239389)
