Clausal Temporal Resolution
Michael Fisher (1), Clare Dixon (1), Martin Peim (2) ((1) Department, of Computing, Mathematics, Manchester Metropolitan University, Manchester,, UK, (2) Department of Computer Science, Victoria University of Manchester,, Manchester, UK)
TL;DR
This paper develops a clausal resolution method for discrete linear temporal logic, including a normal form, translation procedures, and novel resolution rules, with analysis of correctness and complexity.
Contribution
It introduces a new resolution-based approach for temporal logic, including a normal form and resolution rules, advancing automated reasoning in this domain.
Findings
Resolution rules are proven correct.
Normal form preserves satisfiability.
Complexity analysis of the approach.
Abstract
In this article, we examine how clausal resolution can be applied to a specific, but widely used, non-classical logic, namely discrete linear temporal logic. Thus, we first define a normal form for temporal formulae and show how arbitrary temporal formulae can be translated into the normal form, while preserving satisfiability. We then introduce novel resolution rules that can be applied to formulae in this normal form, provide a range of examples and examine the correctness and complexity of this approach is examined and. This clausal resolution approach. Finally, we describe related work and future developments concerning this work.
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, programming, and type systems · Logic, Reasoning, and Knowledge · Formal Methods in Verification