scientific article
From MaRDI portal
Publication:3710510
zbMath0585.03008MaRDI QIDQ3710510
Publication date: 1985
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
branching time temporal logicpropositional temporal logiclinear time temporal logicapplications to Computer Scienceextensions of linear time temporal logictableau decision method
Modal logic (including the logic of norms) (03B45) Abstract data types; algebraic specification (68Q65) Decidability of theories and sets of sentences (03B25)
Related Items
Optimal Tableau Method for Constructive Satisfiability Testing and Model Synthesis in the Alternating-Time Temporal Logic ATL +, Finite sequent calculi for PLTL, A derivation-loop method for temporal logic, The saturated tableaux for linear miniscope Horn-like temporal logic, Generalized Qualitative Spatio-Temporal Reasoning: Complexity and Tableau Method, More efficient proof-search for sequents of temporal logic, Tableaux for Single-Agent Epistemic PDL with Perfect Recall and No Miracles, An optimal decision procedure for right propositional neighborhood logic, Safraless LTL synthesis considering maximal realizability, Programming in metric temporal logic, A tableau construction for finite linear-time temporal logic, Tableaux for realizability of safety specifications, A tableau-based decision procedure for CTL\(^*\), An explicit transition system construction approach to LTL satisfiability checking, Proving correctness of labeled transition systems by semantic tableaux, Explaining counterexamples using causality, A tableau calculus for first-order branching time logic, Loop-type sequent calculi for temporal logic, TABLEAUX: A general theorem prover for modal logics, Interval logics and their decision procedures. I: An interval logic, Interval logics and their decision procedures. II: A real-time interval logic, Search strategies for resolution in temporal logics, One-pass Context-based Tableaux Systems for CTL and ECTL, Model Theoretic Syntax and Parsing, Tableau-Based Procedure for Deciding Satisfiability in the Full Coalitional Multiagent Epistemic Logic, A Labeled Natural Deduction System for a Fragment of CTL *, One-pass and tree-shaped tableau systems for TPTL and \(\mathrm{TPTL_b+Past}\), A general tableau method for propositional interval temporal logics: theory and implementation, Linear temporal logic as an executable semantics for planning languages, Event-based time-stamped claim logic, Saturated calculus for Horn-like sequents of a complete class of a linear temporal first order logic, Realizability of Real-Time Logics, Similarity saturation for first order linear temporal logic with UNLESS, Deductive verification of simple foraging robotic behaviours, Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models, Invertible infinitary calculus without loop rules for restricted FTL, Rasiowa-Sikorski deduction systems in computer science applications., Loop-check specification for a sequent calculus of temporal logic
