Unification in linear temporal logic LTL
From MaRDI portal
Publication:716499
DOI10.1016/j.apal.2011.06.004zbMath1241.03014MaRDI QIDQ716499
Sergey Babenyshev, Vladimir Vladimirovich Rybakov
Publication date: 22 September 2011
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.apal.2011.06.004
03B70: Logic in computer science
03B44: Temporal logic
03F52: Proof-theoretic aspects of linear logic and other substructural logics
Related Items
KD is nullary, DECIDABILITY OF ADMISSIBILITY: ON A PROBLEM BY FRIEDMAN AND ITS SOLUTION BY RYBAKOV, Unification in Linear Modal Logic on Non-transitive Time with the Universal Modality, Unification and admissible rules for paraconsistent minimal Johanssons' logic J and positive intuitionistic logic \(\mathbf{IPC}^+\), On unification and admissible rules in Gabbay-de Jongh logics, Best unifiers in transitive modal logics, Inference rules in Nelson's logics, admissibility and weak admissibility, Admissibility via natural dualities, Admissibility and Unifiability in Contact Logics
Cites Work
- Unnamed Item
- Unification, finite duality and projectivity in varieties of Heyting algebras
- Complexity of admissible rules
- Problems of substitution and admissibility in the modal system Grz and in intuitionistic propositional calculus
- Linear temporal logic with until and next, logical consecutions
- Proof theory for admissible rules
- A criterion for admissibility of rules in the modal system S4 and intuitionistic logic
- Best solving modal equations
- Temporal logic and state systems
- Fast algorithms for uniform semi-unification
- On the admissible rules of intuitionistic propositional logic
- Unification in the Description Logic EL
- Unification in a Description Logic with Transitive Closure of Roles
- A Resolution/Tableaux Algorithm for Projective Approximations in IPC
- A Tableau Method for Checking Rule Admissibility in S4
- Independent Bases of Admissible Rules
- Multi-modal and Temporal Logics with Universal Formula--Reduction of Admissibility to Validity and Unification
- A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments
- Admissible Rules of Lukasiewicz Logic
- The complexity of propositional linear temporal logics
- Rules of inference with parameters for intuitionistic logic
- Unification in intuitionistic logic
- Unification through projectivity
- Computer Science Logic
- Admissible Rules of Modal Logics
- Nominal Unification from a Higher-Order Perspective
- Automated Synthesis of Tableau Calculi
- Unification of concept terms in description logics
