PhD in Computer Science
University of Manchester
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
On to Research Intrests
Part of Lilia Georgieva's Home Page
March 4, 2004