Monodic temporal resolution

DOI10.1145/1119439.1119443MaRDI QIDQ5277744zbMATH OpenOpenAlexFDO

Authors

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

automated theorem provingresolutiontemporal logic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Temporal logic (03B44)

Abstract: Until recently, First-Order Temporal Logic (FOTL) has been little understood. While it is well known that the full logic has no finite axiomatisation, a more detailed analysis of fragments of the logic was not previously available. However, a breakthrough by Hodkinson et.al., identifying a finitely axiomatisable fragment, termed the monodic fragment, has led to improved understanding of FOTL. Yet, in order to utilise these theoretical advances, it is important to have appropriate proof techniques for the monodic fragment. In this paper, we modify and extend the clausal temporal resolution technique, originally developed for propositional temporal logics, to enable its use in such monodic fragments. We develop a specific normal form for formulae in FOTL, and provide a complete resolution calculus for formulae in this form. Not only is this clausal resolution technique useful as a practical proof technique for certain monodic classes, but the use of this approach provides us with increased understanding of the monodic fragment. In particular, we here show how several features of monodic FOTL are established as corollaries of the completeness result for the clausal temporal resolution method. These include definitions of new decidable monodic classes, simplification of existing monodic classes by reductions, and completeness of clausal temporal resolution in the case of monodic logics with expanding domains, a case with much significance in both theory and practice.

Recommendations

• Automated Deduction – CADE-20
• scientific article; zbMATH DE number 1882041
• Automated Reasoning
• Mechanising first-order temporal resolution
• Monodic temporal resolution.

Cited in

(22)

• Axiomatizing the monodic fragment of first-order temporal logic
• Parameterized verification of leader/follower systems via first-order temporal logic
• Mechanising first-order temporal resolution
• 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
• Handling equality in monodic temporal resolution
• On temporal logics with data variable quantifications: decidability and complexity
• Temporal Verification of Fault-Tolerant Protocols
• scientific article; zbMATH DE number 1882041 (Why is no real title available?)
• Harald Ganzinger's legacy: contributions to logics and programming
• First-order resolution methods for modal logics
• Fair Derivations in Monodic Temporal Reasoning
• Automated Reasoning
• A calculus for automatic verification of Petri nets based on resolution and dynamic logics
• Automated Deduction – CADE-20
• Monodic temporal resolution.
• Refutation-aware Gentzen-style calculi for propositional until-free linear-time temporal logic
• Deciding the existence of interpolants and definitions in first-order modal logic
• Bounded linear-time temporal logic: a proof-theoretic investigation
• Quantified epistemic logics for reasoning about knowledge in multi-agent systems

This page was built for publication: Monodic temporal resolution

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5277744)