Resolution for Branching Time Temporal Logics: Applying the Temporal Resolution Rule

We propose algorithms to implement a branching time temporal resolution theorem prover. The branching time temporal logic considered is Computation Tree Logic (CTL), often regarded as the simplest useful logic of this class. Unlike the majority of the research into temporal logic, we adopt a resolution-based approach. The method applies step and temporal resolution rules to the set of formulae in a normal form. Whilst step resolution is similar to the classical resolution rule, the temporal resolution rule resolves a formula, /spl phi/, that must eventually occur with a set of formulae that together imply that /spl phi/ can never occur. Thus the method is dependent on the efficient detection of such sets of formulae. We present algorithms to search for these sets of formulae, give a correctness argument, and examples of their operation.

Authors

• Alexander Bolotov
• Clare Dixon

Keywords

• Logic
• Mathematics
• Concurrent computing
• Power system modeling
• Automata
• Detection algorithms
• DH-HEMTs
• Temporal Logic
• Normal Form
• Set Of Formulas
• Step Resolution
• Right-hand
• Left Side
• Right-hand Side
• Search Algorithm
• Left-hand Side
• Distribution System
• State Model
• Hand Side
• Index Set
• Moment In Time
• State Machine
• Resolution Methods
• Emptiness
• Future Path
• Breadth-first Search
• Unified Algorithm
• Propositional Logic
• Temporal Operators
• Deductive Methods
• Classical Logic