Clausal temporal resolution
Top Cited Papers
- 1 January 2001
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Computational Logic
- Vol. 2 (1) , 12-56
- https://doi.org/10.1145/371282.371311
Abstract
In this article, we examine how clausal resolution can be applied to a specific, but widely used, nonclassical 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. Finally, we describe related work and future developments concerning this work.Keywords
All Related Versions
This publication has 16 references indexed in Scilit:
- Resolution for temporal logics of knowledgeJournal of Logic and Computation, 1998
- A Normal Form for Temporal Logics and its Applications in Theorem-Proving and ExecutionJournal of Logic and Computation, 1997
- The model checker SPINIEEE Transactions on Software Engineering, 1997
- Nonclausal deduction in first-order temporal logicJournal of the ACM, 1990
- The complementation problem for Büchi automata with applications to temporal logicTheoretical Computer Science, 1987
- A Structure-preserving Clause Form TranslationJournal of Symbolic Computation, 1986
- The complexity of propositional linear temporal logicsJournal of the ACM, 1985
- The decision problem for linear temporal logic.Notre Dame Journal of Formal Logic, 1985
- Specifying Concurrent Program ModulesACM Transactions on Programming Languages and Systems, 1983
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965