Kombination von Aktionsformalismen und Beschreibungslogiken zur Entwicklung von Methoden zum Schließen über Aktionen in komplexen, strukturierten Umgebungen

• Applicant: Professor Dr.-Ing. Franz Baader
• Subject Area: Theoretical Computer Science
• Term: from 2007 to 2011
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 56502071

• Final Report Year: 2012

Final Report Abstract

Ziel des Gesamtprojektes ware es, durch die Kombination von Aktionsformalismen und Beschreibungslogiken effiziente Methoden zum Schließen über Aktionen in komplexen, strukturierten Umgebungen zu entwickeln. Dazu wurden Aktionsformalismen betrachtet, die aus dem Fluentkalkül dadurch entstehen, dass die Basislogik von Prädikatenlogik erster Stufe auf eine geeignete Beschreibungslogik eingeschränkt wird. Die im Antrag für die erste Projektphase geäußerte Hoffnung, dass dadurch - im Unterschied zum vollen Fluentkalkül - relevante Schlussfolgerungsprobleme in dem so erhaltenen Aktionsformalismus entscheidbar werden, wurde durch die Arbeiten in der ersten Phase bestätigt. Allerdings wurden dabei auch Probleme lokalisiert, die in der zweiten Projektphase angegangen werden sollten. Zum einen hatten wir festgestellt, dass bei Verwendung ausdrucksstarker terminologischer Formalismen das so genannte Ramifikationsproblem (d. h. das Problem der Behandlung indirekter Effekte von Aktionen) auftritt, das sowohl die Definition der Semantik als auch die algorithmische Behandlung des Formalismus erschwert. Zum anderen waren die in der ersten Phase entwickelten Algorithmen teilweise von sehr hoher Komplexität und damit nicht unbedingt praktikabel. In der zweiten Projektphase wurde das Ramifikationsproblem dadurch gelöst, dass sogenannte Kausalbeziehungen als zusätzliche Komponenten einer beschreibungslogischen Aktionstheorie eingeführt wurden. Bzgl. der Komplexität der in der ersten Phase entwickelten Algorithmen untersuchten wir in der zweiten Phase einerseits, wie die Existenz- und Komplexitätsresultate für Update-ABoxen durch Abschwächung der Anforderungen an diese verbessert werden können. Es stellte sich heraus, dass insbesondere die projektiven Update-ABoxen, welche zusätzliche Hilfssymbole enthalten dürfen, zu wesentlich besseren Resultaten führen. Andererseits betrachteten wir auch beschreibungslogische Aktionstheorien, bei der die Basislogik auf die polynomiell entscheidbare Beschreibungslogik EL eingeschränkt war. Leider bestätigte sich hier unsere Hoffnung nicht, dass für diese eingeschränkten Aktionstheorien Inferenzprobleme wie das Projektionsproblem ebenfalls polynomiell entscheidbar sind. In der zweiten Projektphase wurde auch eine kalkülunabhängige, deklarative Agentenprogrammiersprache entwickelt, die es erlaubt, Agentenlogikprogramme (ALPs) zu schreiben. Diese wurde für den Fall von ALPs für Aktionstheorien in dem auf ABox Updates eingeschränkten Fluentkalkül implementiert. Dies erforderte auch die Implementierung und Optimierung der Algorithmen zur Berechnung von Updatea Aboxen und deren Konsequenzen. Zusätzlich wurde die Aktionsprogrammiersprache um eine einfache Planungskomponente erweitert. Desweiteren wurde in der zweiten Projektphase eine neue temporale Beschreibungslogik mit guten algorithmischen Eigenschaften entwickelt und deren Anwendung für die Runtime-Verifikation und die Verifikation von Aktionsprogrammen untersucht.

Publications

• (2007). Integrating action calculi and description logics. In: Hertzberg, J., Beetz, M., and Englert, R., editors, Proceedings of the 30th Annual German Conference on Artificial Intelligence (KI 2007), volume 4667 of LNCS, pages 68–83, Osnabrück, Germany. Springer
  Drescher, C. and Thielscher, M.
  
• (2009). A declarative agent programming language based on action theories. In: Ghilardi, S. and Sebastiani, R., editors, Proceedings of the Seventh International Symposion on Frontiers of Combining Systems (FroCoS 2009), volume 5749 of LNCS, pages 230–245, Trento, Italy. Springer
  Drescher, C., Schiffel, S., and Thielscher, M.
  
• (2009). Putting ABox updates into action. In: Ghilardi, S. and Sebastiani, R., editors, Proceedings of the Seventh International Symposion on Frontiers of Combining Systems (FroCoS 2009), volume 5749 of LNCS, pages 214–229, Trento, Italy. Springer
  Drescher, C., Liu, H., Baader, F., Guhlemann, S., Petersohn, U., Steinke, P., and Thielscher, M.
  
• (2010). Using Causal Relationships to Deal with the Rau mification Problem in Action Formalisms Based on Description Logics. In: Christian G. Fermüller and Andrei Voronkov, editors, Proceedings of the 17th International Conference on Logic for Programming, Artifical Intelligence, and Reasoning (LPAR-17), volume 6397 of LNCS, pages 82–96, Yogyakarta, Indonesia. Springer
  Baader, F., Lippmann, M., and Liu, H.
  
• (2010). Verifying Properties of Infinite Sequences of Description Logic Actions. In: Helder Coelho, Rudi Studer, and Michael Wooldridge, editors, Proceedings of the 19th European Conference on Artificial Intelligence (ECAI10), pages 53–58, Lisbon, Portugal. IOS Press
  Baader, F., Liu, H., and ul Mehdi, A.
  
• (2011). A unifying action calculus. Artificial Intelligence. 175(1): 120–141 (2011)
  Thielscher, M.