Monodic temporal resolution

DOI10.1145/1119439.1119443zbMath1367.03035arXivcs/0306041MaRDI QIDQ5277744

No author found.

Publication date: 12 July 2017

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/cs/0306041

zbMATH Keywords

resolution; temporal logic; automated theorem proving

Mathematics Subject Classification ID

03B35: Mechanization of proofs and logical operations

03B44: Temporal logic

Related Items

Harald Ganzinger’s Legacy: Contributions to Logics and Programming, First-Order Resolution Methods for Modal Logics, Fair Derivations in Monodic Temporal Reasoning, Refutation-aware Gentzen-style calculi for propositional until-free linear-time temporal logic, On temporal logics with data variable quantifications: decidability and complexity, A calculus for automatic verification of Petri nets based on resolution and dynamic logics, Bounded linear-time temporal logic: a proof-theoretic investigation, Quantified epistemic logics for reasoning about knowledge in multi-agent systems, Parameterized verification of leader/follower systems via first-order temporal logic, Theorem proving using clausal resolution: from past to present, Temporal Logics of Knowledge and their Applications in Security, A Cookbook for Temporal Conceptual Data Modelling with Description Logics, Undecidable Propositional Bimodal Logics and One-Variable First-Order Linear Temporal Logics with Counting, Temporal Verification of Fault-Tolerant Protocols