Monodic temporal resolution
Anatoly Degtyarev, Michael Fisher, and Boris Konev

TL;DR
This paper extends a resolution technique to monodic fragments of First-Order Temporal Logic, enabling practical proof methods and deepening theoretical understanding of these fragments, especially with expanding domains.
Contribution
It develops a complete resolution calculus for monodic FOTL, facilitating proof procedures and theoretical insights into decidable classes and domain expansions.
Findings
Complete resolution calculus for monodic FOTL
Decidable classes of monodic FOTL identified
Resolution completeness for expanding domains
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Advanced Algebra and Logic · Logic, programming, and type systems
