An Algorithm for Guiding Clausal Temporal Resolution

TitleAn Algorithm for Guiding Clausal Temporal Resolution
Publication TypeConference Paper
Year of Publication2001
AuthorsC. Fernandez-Gago, M. Fisher, and C. Dixon
Conference Name4th International Workshop on Strategies in Automated Deduction (STRATEGIES’01)
Date PublishedJune
Conference LocationSiena, Italy
Abstract

The clausal resolution method developed for discrete temporal log- ics involves translation to a normal form, classical resolution on formulae within states (termed step resolution) and temporal resolution between states. Step res- olution may generate an unnecessarily large set of clauses. In addition, the most expensive part of the method is the application of the temporal resolution oper- ation. In this paper we develop an algorithm to guide the search for the set of clauses needed for the application of temporal resolution. The algorithm is based on the outputs of a refined temporal resolution rule which allows us to generate temporal resolvents earlier within the process. In particular, this can also help us to avoid unnecessary step resolution and focus search for the most relevant clauses.

Citation KeyFernandez01
Paper File: 
https://nics.uma.es:8082/sites/default/files/papers/Fernandez01.pdf