Clausal temporal resolution
From MaRDI portal
Publication:5738910
DOI10.1145/371282.371311zbMath1365.03017arXivcs/9907032OpenAlexW2131225255WikidataQ98283991 ScholiaQ98283991MaRDI QIDQ5738910
No author found.
Publication date: 13 June 2017
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/cs/9907032
Related Items (34)
Extracting unsatisfiable cores for LTL via temporal resolution ⋮ A derivation-loop method for temporal logic ⋮ A Cookbook for Temporal Conceptual Data Modelling with Description Logics ⋮ Temporal abductive reasoning about biochemical reactions ⋮ One-Pass Tableaux for Computation Tree Logic ⋮ A survey on temporal logics for specifying and verifying real-time systems ⋮ Refutation-aware Gentzen-style calculi for propositional until-free linear-time temporal logic ⋮ On feasible cases of checking multi-agent systems behavior. ⋮ Deciding FO-rewritability of Regular Languages and Ontology-Mediated Queries in Linear Temporal Logic ⋮ Towards a notion of unsatisfiable and unrealizable cores for LTL ⋮ Theorem proving using clausal resolution: from past to present ⋮ An explicit transition system construction approach to LTL satisfiability checking ⋮ Backdoors for linear temporal logic ⋮ Loop-type sequent calculi for temporal logic ⋮ First-order rewritability of ontology-mediated queries in linear temporal logic ⋮ Enhancing unsatisfiable cores for LTL with information on temporal relevance ⋮ A resolution calculus for the branching-time temporal logic CTL ⋮ Verification and enforcement of access control policies ⋮ First-Order Resolution Methods for Modal Logics ⋮ Mechanising first-order temporal resolution ⋮ Alternating automata and temporal logic normal forms ⋮ Using temporal logics of knowledge for specification and verification -- a case study ⋮ A Refined Resolution Calculus for CTL ⋮ Fair Derivations in Monodic Temporal Reasoning ⋮ Variable and clause elimination for LTL satisfiability checking ⋮ \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments ⋮ Bounded linear-time temporal logic: a proof-theoretic investigation ⋮ Tableaux for logics of time and knowledge with interactions relating to synchrony ⋮ Deductive verification of simple foraging robotic behaviours ⋮ Temporal similarity by measuring possibilistic uncertainty in CBR ⋮ Verification from Declarative Specifications Using Logic Programming ⋮ SAT-based explicit LTL reasoning and its application to satisfiability checking ⋮ Temporal Logics of Knowledge and their Applications in Security ⋮ Clausal resolution in a logic of rational agency
This page was built for publication: Clausal temporal resolution
