Tech Reports

ULCS-08-010

First-order Resolution for CTL

Lan Zhang, Ullrich Hustadt and Clare Dixon

Abstract

In this paper, we describe an approach to theorem proving in Computational Tree Logic (CTL) which utilises classical first-order resolution techniques. Since there already exist a lot of well-developed first-order logic theorem provers, reusing those techniques provides great benefit for solving other similar problems. We do not attempt to prove CTL theorems directly within the temporal logic syntax. We first translate arbitrary CTL formulae into a normal form for CTL and then implement the CTL calculus using resolution in first-order logic. After that, we utilise an efficient first-order logic theorem prover, for example, VAMPIRE or SPASS to carry out proof. Further, this approach has the potential to be extended to solve problems in other logics.

For each technical report listed here, copyright and all intellectual property rights remain with the respective authors. Copyright is effective from the year of publication in each case. By downloading a file from this page, you agree to use it only for purposes of research and scholarship. Any other use of this material or storage of it in any medium or its sale or distribution in any form is expressly forbidden without prior written permission from the authors concerned.