PhD in Computer Science
University of Manchester
April 2003.

Topic: ``Reasoning about Guarded Formulae''

We study hyperresolution as a decision procedure and a model generation procedure for subfragments of the guarded fragment. We develop a decision procedure, which corresponds to tableau procedures that are common in modal logics and knowledge representation. We show that the procedure is a model builder for satisfiable guarded formulae and that it can be refined so that only minimal Herbrand models are generated. Using a suitable control strategy, we optimise the procedure and obtain a decision procedure for guarded formulae with polynomial space complexity.
The decision procedure has concrete application domains. It provides a framework for reasoning about very expressive modal and description logics with role inverse that can be embedded into the guarded fragment. We show that the decidability and model building results can be extended to a new clausal class BU, which allows for the embedding of formulae outside the guarded fragment and its extensions.

MSc in Computer Science
University of Sofia
July 1999.

On to Research Intrests Part of Lilia Georgieva's Home Page
March 4, 2004