A Resolution Method for Temporal Logic

Fisher, Michael

A Resolution Method for Temporal Logic

Download BibTeX Cite

Proceedings of the Twelfth International Joint Conference on Artificial Intelligence. Automated Reasoning. Pages 99-103.

Abstract

In this paper, a resolution method for propositional temporal logic is presented. Temporal formulae, incorporating both past-time and future-time temporal operators, are converted to Separated Normal Form (SNF), then both non-temporal and temporal resolution rules are applied. The resolution method is based on classical resolution, but incorporates a temporal resolution rule that can be implemented efficiently using a graph-theoretic approach.

Michael Fisher. 1991. A Resolution Method for Temporal Logic. In Proceedings of the Twelfth International Joint Conference on Artificial Intelligence, IJCAI-91. IJCAI, 99–103. https://ijcai.org/proceedings/1991/15

@inproceedings{ijcai1991p15,
  title     = {A Resolution Method for Temporal Logic},
  author    = {Fisher, Michael},
  booktitle = {Proceedings of the Twelfth International Joint Conference on
               Artificial Intelligence, {IJCAI-91}},
  publisher = {International Joint Conferences on Artificial Intelligence},
  editor    = {John Mylopoulos and Ray Reiter},
  pages     = {99--103},
  year      = {1991},
  month     = {8},
  note      = {Automated Reasoning},
  url       = {https://ijcai.org/proceedings/1991/15},
}

TY  - CPAPER
TI  - A Resolution Method for Temporal Logic
AU  - Fisher, Michael
T2  - Proceedings of the Twelfth International Joint Conference on Artificial Intelligence, IJCAI-91
PB  - International Joint Conferences on Artificial Intelligence
PY  - 1991
SP  - 99
EP  - 103
UR  - https://ijcai.org/proceedings/1991/15
ER  -