---
title: "A Resolution Method for Temporal Logic"
authors:
  - "Michael Fisher"
doi: ""
url: "https://ijcai.org/proceedings/1991/15"
pdf: "https://ijcai.org/proceedings/1991/0015.pdf"
venue: "Proceedings of the Twelfth International Joint Conference on Artificial Intelligence"
year: 1991
pages: "99-103"
track: "Automated Reasoning"
keywords:
---

# A Resolution Method for Temporal Logic

Michael Fisher

*Proceedings of the Twelfth International Joint Conference on Artificial Intelligence*, 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.