+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Montag, 21.11.2022, 14:00-15:00 Uhr Der öffentliche Vortrag findet hybrid statt: Raum: Raum 5053.2 (B-IT-Hörsaal)/Informatikzentrum, Ahornstraße 55 Zoom: https://rwth.zoom.us/j/96565981989?pwd=b3B3aEVmSnJ1VFJhUDYwSlorbTcvQT09 Meeting-ID: 965 6598 1989 Kenncode: 346594 Referent: Herr Daxin Liu, M. Sc. LuFG Informatik 5 Thema: Projection in a Probabilistic Epistemic Logic and Its Application to Belief-based-Program Verification Abstract: Rich representation of knowledge and actions has been a goal that many AI researchers pursue. Among all proposals, perhaps, the situation calculus by Reiter is the most widely studied, where actions are treated as logical terms and the agent's knowledge is represented by logical formulas. The language has been extended to incorporate many features like time, concurrency, procedures, etc.. Most recently, Belle and Lakemeyer proposed a modal logic DS which deals with degrees of belief and noisy sensing. The logic has many appealing properties like full introspection, however, it also has some shortcomings. Perhaps the main one is the lack of expressiveness when it comes to degrees of belief. Currently, the language allows expressing degrees of belief only as constants making it impossible to express belief distribution. Another important problem is that it lacks projection reasoning mechanisms. Projection is the task to determine whether a query about the future is entailed by an initial knowledge base. Two solutions of projection exist regression and progression. While regression transfers the query about the future into a query about the initial state and evaluates it there, progression transfers the whole initial knowledge base into a future one. In this thesis, we first lift the expressiveness of the logic DS by modifying both the syntax and semantics. Moreover, we investigate the projection problem in DS. In particular, we propose a regression operator which can handle queries with nested beliefs and beliefs with quantifying-in. For progression, we show that classical progression is first-order definable for a fragment of the logic and provide our solution for the progression of belief in terms of only-believing after actions. Moreover, we exploit how to apply the proposed methods in a more practical scenario: on the verification of belief programs, a probabilistic extension of Golog programs, where every action and sensing could be noisy and every test refers to the agent's subjective beliefs. We show that the verification problem is undecidable even in very restrictive settings. We also show a special case where the problem is decidable. Es laden ein: die Dozentinnen und Dozenten der Informatik _______________________________ Leany Maaßen RWTH Aachen University Lehrstuhl Informatik 5, LuFG Informatik 5 Prof. Dr. Stefan Decker, Prof. Dr. Matthias Jarke, Prof. Gerhard Lakemeyer Ph.D., JunProf. Dr. Sandra Geisler Ahornstrasse 55 D-52074 Aachen Tel: 0241-80-21509 Fax: 0241-80-22321 E-Mail: maassen@dbis.rwth-aachen.de