Pages that link to "Item:Q2753601"
From MaRDI portal
The following pages link to Tableau methods for modal and temporal logics (Q2753601):
Displaying 50 items.
- Tableau reductions: towards an optimal decision procedure for the modal necessity (Q313007) (← links)
- ExpTime tableaux for \(\mathcal {ALC}\) using sound global caching (Q352943) (← links)
- Invariant-free clausal temporal resolution (Q352974) (← links)
- Labeled sequent calculi for modal logics and implicit contractions (Q377468) (← links)
- Tableaux and hypersequents for justification logics (Q408538) (← links)
- Prefixed tableaus and nested sequents (Q409323) (← links)
- First-order intensional logic (Q598308) (← links)
- Cut elimination in coalgebraic logics (Q618171) (← links)
- Complexity of hybrid logics over transitive frames (Q631089) (← links)
- Proof analysis in intermediate logics (Q661286) (← links)
- ExpTime tableau decision procedures for regular grammar logics with converse (Q763333) (← links)
- Symmetric blocking (Q897931) (← links)
- Cut-free sequent systems for temporal logic (Q941433) (← links)
- The method of Socratic proofs for modal propositional logics: K5, S4.2, S4.3, S4F, S4R, S4M and G. (Q1005938) (← links)
- Proof theory for admissible rules (Q1023055) (← links)
- Dual systems of tableaux and sequents for PLTL (Q1035676) (← links)
- A new methodology for developing deduction methods (Q1037405) (← links)
- Cut elimination for \(\mathrm{S4}_n\) and \(\mathrm{K4}_n\) with the central agent axiom (Q1042695) (← links)
- Hyperresolution for guarded formulae (Q1404983) (← links)
- EXPtime tableaux for ALC (Q1589576) (← links)
- Pure modal logic of names and tableau systems (Q1756600) (← links)
- On refutation rules (Q1941727) (← links)
- Constrained consequence (Q1941731) (← links)
- Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\) (Q1989347) (← links)
- Cut-elimination for weak Grzegorczyk logic Go (Q2016062) (← links)
- Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models (Q2095426) (← links)
- Local is best: efficient reductions to modal logic \textsf{K} (Q2102930) (← links)
- Local reductions for the modal cube (Q2104538) (← links)
- A formally verified cut-elimination procedure for linear nested sequents for tense logic (Q2142082) (← links)
- Tableaux for some modal-tense logics Graham Priest's fashion (Q2144188) (← links)
- Uniform interpolation via nested sequents (Q2148805) (← links)
- Proofs and countermodels in non-classical logics (Q2254557) (← links)
- A loop-free decision procedure for modal propositional logics K4, S4 and S5 (Q2271187) (← links)
- Labelled tableau systems for some subintuitionistic logics (Q2334660) (← links)
- In all but finitely many possible worlds: model-theoretic investigations on `\textit{overwhelming majority}' default conditionals (Q2398203) (← links)
- The modal logic of copy and remove (Q2401633) (← links)
- Tableaux for constructive concurrent dynamic logic (Q2488268) (← links)
- Deciding regular grammar logics with converse through first-order logic (Q2567343) (← links)
- Complexity of modal logics with Presburger constraints (Q2638188) (← links)
- Modal logic S5 in answer set programming with lazy creation of worlds (Q2694545) (← links)
- (Q2721192) (← links)
- On the Complexity of the Equational Theory of Residuated Boolean Algebras (Q2820699) (← links)
- Tableau method and NEXPTIME-completeness of DEL-sequents (Q2825404) (← links)
- Query answering with DBoxes is hard (Q2825409) (← links)
- Testing XML constraint satisfiability (Q2867947) (← links)
- Designing tableau-like axiomatization for propositional linear temporal logic at home of Arthur Prior (Q2880593) (← links)
- Tableaux for Reasoning about Atomic Updates (Q2996198) (← links)
- A History of Until (Q3185767) (← links)
- Coalition Description Logic with Individuals (Q3185771) (← links)
- Intuitionistic Decision Procedures Since Gentzen (Q3305556) (← links)