Examiners:
Dov Gabbay (Augustus De Morgan Professor of Logic at King's College) Tito Toro (Professor at the Manchester Metropolitan University) Renate Shmidt (Lecturer at the University of Manchester)
Abstract

Getting my thesis

Related publications 
Clausal Resolution approach was developed by M.Fisher inM. Fisher. A Resolution Method for Temporal Logic ,
(in Proceedings of Twelfth International Joint Conference on Artificial Intelligence (IJCAI) , held in Sydney, Australia, August 1991. Published by Morgan Kaufmann).Fisher, M. A Normal Form for Temporal Logics and its Applications in TheoremProving and Execution. Journal of Logic and Computation, 7(4):429456, August 1997. C. Dixon.
Strategies for Temporal Resolution,
PhD thesis, The University of Manchester, September 1995. Also Technical Report number UMCS95121, ISSN 13616153, Department of Computer Science, University of Manchester, December 1995. (It's a large file so be warned!)Dixon, C.,
Temporal Resolution using a BreadthFirst Search Algorithm,
in the Annals of Mathematics and Artificial Intelligence, volume 22, special issue on Temporal Representation and Reasoning 1998. Baltzer Science Publishers. ISSN 10122443.The key elements of the resolution method, namely the normal form, the concept of step resolution and a novel temporal resolution rule introduced, justified, and applied in the context of the computation tree logic CTL are described in
A.Bolotov and M.Fisher.
A Resolution Method for CTL Branching Time Temporal Logic.
In IV International Workshop on Temporal Representation and Reasoning (TIME'97), Published by the IEEE, 1997. Please note the IEEE copyright.Full version of this paper:
A.Bolotov and M.Fisher.
A Clausal Resolution Method for CTL Branching Time Temporal Logic.
In Journal of Experimental and Theoretical Artificial Intelligence, Taylor & Francis, 11, 1999, pp 7793. Preliminary version is here
A.Bolotov and C.Dixon
Resolution for Branching Time Temporal Logics: Applying the Temporal Resolution Rule.
To appear in the proceedings of TIME2000.Our approach of developing clausal resolution for the full branchingtime logic logic CTL* is described in
A.Bolotov, C.Dixon, and M.Fisher.
Clausal resolution for CTL*. (Please, note the SpringerVerlag copyright.)
Proc. 24th International Symposium on Mathematical Foundations of Computer Science (MFCS'99), volume 1672 of Lecture Notes in Computer Science, pages 137148, SpringerVerlag, 1999.Other related information on research in this area and links can be found in the CARD research group WWWpage.