Clausal Temporal Resolution
Logic in Computer Science
2007-05-23 v2 Artificial Intelligence
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.
Keywords
Cite
@article{arxiv.cs/9907032,
title = {Clausal Temporal Resolution},
author = {Michael Fisher and Clare Dixon and Martin Peim},
journal= {arXiv preprint arXiv:cs/9907032},
year = {2007}
}
Comments
35 pages, 0 figures Expanded related work, corrected typos, expanded proofs