Best unifiers in transitive modal logics
The paper offers a brief analysis of the unification problem in modal transitive logics related to the logic S4. There are two views on the origin of the term ``unification, though both views are very close to each other. Logical unification is the problem to solve whether, for two given formulas, there is a substitution, which makes these formulas equivalent. Unification in computer science is the problem of making two given terms semantically equal. In most cases the problem of term unification directly coincides with its logical unification counterpart. The unification problem is in fact a particular case of a more complicated problem: the substitution problem. That is, the problem whether a formula can be made a theorem after replacing some of the variables by formulas. Ghilardi studied unification in propositional modal logics with the aim of describing all possible unifiers. His approach is very useful in dealing with admissibility. In fact, when a computable finite set of best unifiers is constructed, a solution of the admissibility problem follows immediately. The results of Ghilardi on unification gave a computational ground to construct all unifiers. These techniques turned out to be effective tools to work with various problems. In this paper the author answers positively to the following question: do his previous algorithms for deciding admissibility of inference rules work for the computation of best unifiers in modal transitive logics?
- Unifiers in transitive modal logics for formulas with coefficients (meta-variables)
- Transparent unifiers in modal logics with self-conjugate operators
- scientific article; zbMATH DE number 1189062
- Unification in first-order transitive modal logic
- Filtering unification and most general unifiers in modal logic
- A criterion for admissibility of rules in the modal system S4 and intuitionistic logic
- A Machine-Oriented Logic Based on the Resolution Principle
- A tableau method for checking rule admissibility in S4
- Admissible Rules of Lukasiewicz Logic
- Admissible Rules of Modal Logics
- Best solving modal equations
- Complexity of finite-variable fragments of EXPTIME-complete logics
- Computer Science Logic
- Fast algorithms for uniform semi-unification
- Handbook of modal logic
- scientific article; zbMATH DE number 1936671 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- Independent Bases of Admissible Rules
- Linear temporal logic LTL: basis for admissible rules
- Linear temporal logic with until and next, logical consecutions
- Logical equations and admissible rules of inference with parameters in modal provability logics
- Multi-modal and Temporal Logics with Universal Formula--Reduction of Admissibility to Validity and Unification
- N-Prolog: An extension of Prolog with hypothetical implications. I.
- On the admissible rules of intuitionistic propositional logic
- Problems of substitution and admissibility in the modal system Grz and in intuitionistic propositional calculus
- Proof theory for admissible rules
- Rules of inference with parameters for intuitionistic logic
- Temporal logic and state systems
- Term Rewriting and All That
- Unification in a description logic with transitive closure of roles
- Unification in intuitionistic logic
- Unification in linear temporal logic LTL
- Unification in the description logic EL
- Unification of concept terms in description logics
- Unification theory
- Unification through projectivity
- Unification, finite duality and projectivity in varieties of Heyting algebras
- Unification in pretabular extensions of S4
- A syntactic approach to unification in transitive reflexive modal logics
- Unifiers in transitive modal logics for formulas with coefficients (meta-variables)
- DECIDABILITY OF ADMISSIBILITY: ON A PROBLEM BY FRIEDMAN AND ITS SOLUTION BY RYBAKOV
- Unification in first-order transitive modal logic
- Filtering unification and most general unifiers in modal logic
- UNIFICATION IN SUPERINTUITIONISTIC PREDICATE LOGICS AND ITS APPLICATIONS
- Transparent unifiers in modal logics with self-conjugate operators
- Projective unification in weakly transitive and weakly symmetric modal logics
- 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: Best unifiers in transitive modal logics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q647403)
