Abstract
An approach to applying clausal resolution, a proof method well suited to mechanisation, to temporal logics has been developed by Fisher. The method involves translation to a normal form, classical style resolution within states, and temporal resolution between states. Not only has it been shown to be correct but as it consists of only one temporal resolution rule, it is particularly suitable as the basis of an automated temporal resolution theorem prover. As the application of the temporal resolution rule is the most costly part of the method, it is on this area that we focus. Detailed algorithms for a breadth-first search approach to the application of this rule are presented. Correctness is shown and complexity given. Analysis of the behaviour of the algorithms is carried out and we explain why this approach is an improvement to others suggested.
| Original language | English |
|---|---|
| Pages (from-to) | 87-115 |
| Number of pages | 29 |
| Journal | Annals of Mathematics and Artificial Intelligence |
| Volume | 22 |
| Issue number | 1-2 |
| Publication status | Published - 1998 |
Keywords
- Temporal Logic
- Model checking
- Stit