Temporal Resolution: A Breadth-First Search Approach

An approach to applying clausal resolution, a proof method for classical logics 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. The method consists of only one temporal resolution rule and is therefore particularly suitable as the basis of an automated temporal resolution theorem prover. As the application of this temporal resolution rule is the most costly part of the method, involving search amongst graphs, it is on this area we focus. A breadth-first search approach to the application of this rule is presented and shown to be correct. Analysis of its operation is carried out and test results for its comparison to a previously developed depth-first style algorithm given.

Authors

• Clare Dixon

Keywords

• Logic testing
• Algorithm design and analysis
• System testing
• System recovery
• Automata
• Explosions
• Breadth-first Search
• Breadth-first Search Approach
• Application Of Rules
• Depth-first
• Temporal Logic
• Classical Logic
• Right-hand
• Left Side
• Right-hand Side
• Search Algorithm
• Left-hand Side
• Set Of Rules
• Hand Side
• Moment In Time
• Normal Form
• Resolution Methods
• Beginning Of Time
• State Index
• First-order Logic
• Prototype Implementation
• Propositional Logic
• Step Resolution
• Set Of Formulas
• Resolution Step
• Previous Moment