Unification in linear temporal logic LTL
From MaRDI portal
Publication:716499
DOI10.1016/j.apal.2011.06.004zbMath1241.03014OpenAlexW1989441839MaRDI 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
Logic in computer science (03B70) Temporal logic (03B44) Proof-theoretic aspects of linear logic and other substructural logics (03F52)
Related Items (10)
Admissibility and Unifiability in Contact Logics ⋮ 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 ⋮ KD is nullary ⋮ Satisfiability problem in interval FP-logic ⋮ Best unifiers in transitive modal logics ⋮ Unification in Linear Modal Logic on Non-transitive Time with the Universal Modality ⋮ DECIDABILITY OF ADMISSIBILITY: ON A PROBLEM BY FRIEDMAN AND ITS SOLUTION BY RYBAKOV ⋮ Inference rules in Nelson's logics, admissibility and weak admissibility ⋮ Admissibility via natural dualities
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
This page was built for publication: Unification in linear temporal logic LTL
