Previous ...
Blocking mechanisms in description logics, a general approach
Dmitry Tishkovsky - 11.6.2008
We will take a close look on various standard mechanism of blocking
in tableaux for various description logics and attemt to simulate
these mechanisms by a general blocking rule - the unrestricted
blocking rule. In particular, we will consider static and dynamic,
subset and equality, and successor and anywhere blocking mechanisms.
Reasoning about actions and knowlege: Multi-agent dynamic logics with informational test
Dmitry Tishkovsky - 9.6.2008
The logics are based on a new formalisation and semantics of the
test operator of propositional dynamic logic and a representation
of actions which distinguishes abstract actions from concrete actions.
The new test operator, called informational test, can be used
to formalise the beliefs and knowledge of particular agents
as dynamic modalities.
This approach is consistent with the formalisation of the agents`
beliefs and knowledge as K(D)45 and S5 modalities.
Properties concerning informativeness, truthfulness and preservation
of beliefs were proved for a derivative of the informational test
operator.
It was shown that common belief and common knowledge can be expressed
in the considered logics. This means, the logics are more expressive
than propositional dynamic logic with an extra modality for belief
or knowledge.
The logics remain decidable and belong to 2EXPTIME.
Versions of the considered logics express natural additional properties
of beliefs or knowledge and interaction of beliefs or knowledge
with actions.
It was shown that a simulation of PDL can be constructed in one
of these extensions.
A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments
Dmitry Tishkovsky - 11.6.2008
A general method for proving termination of
tableaux-based procedures for modal-type logics and related
first-order fragments will be presented. The method is based on connections between
filtration arguments and a general blocking technique. The method
provides a general framework for developing tableau-based decision
procedures for a large class of logics. In particular, the method
can be applied to many well-known description and modal logics.
The class includes traditional modal logics such as S4 and modal
logics with the universal modality, as well as description logics
such as ALC with nominals and general TBoxes. Also contained
in the class are harder and less well-studied modal logics with
complex modalities and description logics with complex role operators
such as Boolean modal logic, and the description logic ALBO.
In addition, the techniques allow us to specify tableau-based decision
procedures for related solvable fragments of first-order logic,
including the two-variable fragment of first-order logic.
This solves a long-standing open problem.
