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.

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.

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.

Akce

The project members were/are implied in the organization of the following events:

24. 1. – 30. 1. 2009

SOFSEM 2009

Špindlerův Mlýn, Czech Republic

SOFSEM: Current Trends in Theory and Practice of Computer Science

30. 11. – 2. 12. 2008

SEMWEB 2008
(hotel Svratka)

SEMWEB (Fotogalerie)

Výjezdní pracovní seminář projektu programu "Informační společnost" Inteligentní modely, algoritmy, metody a nástroje pro vytváření sémantického webu – závěrečná oponentura:
Role oponentů laskavě přijali prof. Ing. Mária Bieliková, PhD. a doc. Ing. Vojtěch Svátek, Dr.

22. 9. – 26. 9. 2008

ITAT 2008

Hotel Hrebienok, Vysoké Tatry, Slovakia

ITAT: Konferencia o informačných (inteligentných) technológiách – aplikácie a teória

13. 2. – 15. 2. 2008

Znalosti 2008

Bratislava, Slovakia

Znalosti: Konference s odbornou záštitou IFIP, technického výboru 12 pro umělou inteligenci.

20. 1. – 26. 1. 2008

SOFSEM 2008

High Tatras, Slovakia

SOFSEM: Current Trends in Theory and Practice of Computer Science

21. 9. – 27. 9. 2007

ITAT 2007

Polana, Slovakia

ITAT: Konferencia o informačných (inteligentných) technológiách – aplikácie a teória

20. 1. – 26. 1. 2007

SOFSEM 2007

Harrachov, Czech Republic

SOFSEM: Current Trends in Theory and Practice of Computer Science

5. 10. – 7. 10. 2006

SEMWEB 2006

hotel Olympia, Zadov

SEMWEB: Výjezdní pracovní seminář projektu programu "Informační společnost" Inteligentní modely, algoritmy, metody a nástroje pro vytváření sémantického webu

26. 9. – 1. 10. 2006

ITAT 2006

Chata Kosodrevina, Bystrá dolina, Slovakia

ITAT: Seminár z Informačných (inteligentných) technológií – aplikácie a teória

21. 1. – 27. 1. 2006

SOFSEM 2006

Měřín, Czech Republic

SOFSEM: Current Trends in Theory and Practice of Computer Science

SOFSEM (SOFtware SEMinar) is an international conference devoted to the theory and practice of computer science. Its aim is to foster cooperation among professionals from academia and industry working in various areas of computer science.

SOFSEM offers a unique opportunity to obtain quckly a representative overview of the areas of computer science which are selected as the topics of the year

20. 9. – 25. 9. 2005

ITAT 2005

Akademik, Račkova dolina, Slovakia

ITAT: Seminár z Informačných (inteligentných) technológií – aplikácie a teória

15. 9. – 19. 9. 2004

ITAT 2004

Slovakia

ITAT: Workshop on Information Technologies – Applications and Theory