Loading...
Please wait, while we are loading the content...
Similar Documents
Resolution for Branching Time Temporal Logics: Applying the Temporal Resolution Rule (2000)
| Content Provider | CiteSeerX |
|---|---|
| Author | Bolotov, Alexander Bolotov, Er Dixon, Clare |
| Description | In this paper 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, ', that must eventually occur with a set of formulae that together imply that ' 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. |
| File Format | |
| Language | English |
| Publisher | IEEE Computer Society |
| Publisher Date | 2000-01-01 |
| Publisher Institution | In Proceedings of the 7th International Conference on Temporal Representation and Reasoning (TIME2000 |
| Access Restriction | Open |
| Subject Keyword | Useful Logic Temporal Logic Resolution-based Approach Normal Form Branching Time Temporal Logic Classical Resolution Rule Efficient Detection Temporal Resolution Rule Correctness Argument Whilst Step Resolution Computation Tree Logic Present Algorithm |
| Content Type | Text |
| Resource Type | Article |
