Decidable fragments of first-order temporal logics

DOI10.1016/S0168-0072(00)00018-XzbMath0999.03015OpenAlexW2045554431MaRDI QIDQ1591203

Frank Wolter, I. M. Hodkinson, Michael Zakharyashchev

Publication date: 28 November 2002

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0168-0072(00)00018-x

zbMATH Keywords

undecidabilitytemporal databasesdecidabilityfirst-order temporal logicclassical decision problemdecidable fragments

Mathematics Subject Classification ID

Database theory (68P15) Undecidability and degrees of sets of sentences (03D35) Knowledge representation (68T30) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Temporal logic (03B44)

Related Items (46)

A decidable and expressive fragment of Many-Sorted first-order linear temporal logic ⋮ Sound verification procedures for temporal properties of infinite-state systems ⋮ Quantified epistemic logics for reasoning about knowledge in multi-agent systems ⋮ A Decidable Temporal Relevant Logic for Time-Dependent Relevant Human Reasoning ⋮ Undecidability of QLTL and QCTL with two variables and one monadic predicate letter ⋮ First-order temporal verification in practice ⋮ Parameterized verification of leader/follower systems via first-order temporal logic ⋮ Evolving objects in temporal information systems ⋮ On temporal logics with data variable quantifications: decidability and complexity ⋮ On the freeze quantifier in Constraint LTL: Decidability and complexity ⋮ A Cookbook for Temporal Conceptual Data Modelling with Description Logics ⋮ A Conceptual Framework for Secrecy-preserving Reasoning in Knowledge Bases ⋮ Temporal BI: proof system, semantics and translations ⋮ A survey on temporal logics for specifying and verifying real-time systems ⋮ Deciding safety and liveness in TPTL ⋮ A construction of cylindric and polyadic algebras from atomic relation algebras ⋮ Refutation-aware Gentzen-style calculi for propositional until-free linear-time temporal logic ⋮ Бинарный предикат, транзитивное замыкание, две-три переменные: сыграем в домино? ⋮ Are bundles good deals for first-order modal logic? ⋮ Undecidable Propositional Bimodal Logics and One-Variable First-Order Linear Temporal Logics with Counting ⋮ Decidable cases of first-order temporal logic with functions ⋮ Theorem proving using clausal resolution: from past to present ⋮ Constraint LTL satisfiability checking without automata ⋮ Beyond Knowing That: A New Generation of Epistemic Logics ⋮ On the axiomatizability of some first-order spatio-temporal theories ⋮ Serializable histories in quantified propositional temporal logic ⋮ Decidability of infinite-state timed CCP processes and first-order LTL ⋮ Mechanising first-order temporal resolution ⋮ Combining linear-time temporal logic with constructiveness and paraconsistency ⋮ Fair Derivations in Monodic Temporal Reasoning ⋮ Quantification over sets of possible worlds in branching-time semantics ⋮ A Complete Quantified Epistemic Logic for Reasoning about Message Passing Systems ⋮ Checking content consistency of integrated web documents ⋮ First-order expressivity for S5-models: Modal vs. two-sorted languages ⋮ Undecidability of First-Order Intuitionistic and Modal Logics with Two variables ⋮ Temporal Verification of Fault-Tolerant Protocols ⋮ Foundations of Temporal Conceptual Data Models ⋮ First-Order Linear-Time Epistemic Logic with Group Knowledge: An Axiomatisation of the Monodic Fragment ⋮ Bounded linear-time temporal logic: a proof-theoretic investigation ⋮ The serializability problem for a temporal logic of transaction queries ⋮ Deductive verification of simple foraging robotic behaviours ⋮ Propositional epistemic logics with quantification over agents of knowledge (an alternative approach) ⋮ Axiomatizing the monodic fragment of first-order temporal logic ⋮ Complexity of monodic guarded fragments over linear and real time ⋮ Temporal Logics of Knowledge and their Applications in Security ⋮ First-Order Rewritability and Complexity of Two-Dimensional Temporal Ontology-Mediated Queries

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The decision problem for linear temporal logic
• Concerning the semantic consequence relation in first-order temporal logic
• Incompleteness of first-order temporal logic with until
• Temporal aspects of logical procedure definition
• Modal languages and bounded fragments of predicate logic
• A survey of temporal extensions of description logics
• On the feasibility of checking temporal integrity constraints
• Axiomatising first-order temporal logic: Until and since over linear time
• Decidable fragments of first-order modal logics
• On languages with two variables
• Expanded theory of ordered Abelian groups
• Decidability and incompleteness results for first-order temporal logics of linear time
• Products of modal logics, part 1
• A multi-dimensional terminological knowledge representation language
• On the Restraining Power of Guards
• On the elementary theory of linear order
• Elementary properties of ordered abelian groups
• Decidability of Second-Order Theories and Automata on Infinite Trees
• To the memory of Arthur Prior Formal properties of ‘now’

This page was built for publication: Decidable fragments of first-order temporal logics