Knowledge Representation and Reasoning Seminar

In the course students are introduced into reading scientific papers, writing scientific articles, preparing and giving scientific talks, developing research plans, setting up research proposals, etc. These and related topics are discussed with the help of concrete examples taken from the current research issues addressed in the Knowledge Representation and Reasoning Group such as Planning and Concurrency, Reasoning and Acting under Uncertainty, Proof Theory, Computational Logic and Connectionist Systems as well as Cognitive Robotics.

Schedule

If not indicated otherwise, the seminar will take place tuesdays during DS 5 (14.50-16.20) in GRU 350.
Each event should consist of a 45 minutes presentation, followed by a 20 minutes discussion.

Abstracts

• Analysis and extension of algorithms used for theta-subsumption by Georg Rammé on 28. Feb. 2006, 14:50
  After having defined the notion of theta-subsumption, I will describe the principle methods to deal with the NP-completeness of theta-subsumption, and to obtain fast algorithms. I will also present an extended version of an existing algorithm used for theta-subsumption (for datalog clauses), in order to find all substitutions, and by slightly extending the class of allowed clauses by allowing variables and constants in both clauses.
• Towards an Hierarchical Kalman Filter Approach to Robot Localisation and Mapping by Jeannette Bohg on 04. Apr. 2006, 14:50
  The ability of a mobile robot to negotiate its way in an unknown environment largely determines its possible application and performance. The related research area is known as Simultaneous Localisation and Mapping (SLAM). It refers to the task of a mobile robot to continuously build a map of an unknown static environment and to use this map at the same time to localise itself. The long term goal is to develop a SLAM system capable of processing in real time.
  I build upon my previous work where the Extended Kalman Filter (EKF) is utilised for solving the SLAM problem. The major drawback of the EKF is its quadratic complexity in the number of features contained in the map. A popular technique to approach that problem is to subdivide the whole map into submaps. Significant computational savings are made by only operating in a small part of the map.
  The fundamental idea followed in this work, is to apply a submapping approach to a hierarchically structured map. This map consists of rather complex objects, i.e., surfaces, on a higher level, and basic features, i.e., points, on the lowest level. In this example, one submap gathers point features that are situated on the same surface. In a later stage of the navigational process, when the map is sufficiently refined, one surface instead of a dozen points can be utilised for self-localisation.
  I analyse the basic problem of applying the EKF to a two-level hierarchical structure. I will shortly introduce the Compressed Kalman Filter (CKF), a solution to submapping that already uses a two-level representation of the map but does not divide the EKF according to that. The performance of the CKF is evaluated in a simple test scenario. From these experiments, requirements are derived that need to be fulfilled by an algorithm which can handle more than one level. Approaches to fulfil these requirements are presented.
• The Henhouse Project by Tobias Pietzsch and Stephan Saalfeld on 18. Apr. 2006, 14:50
  see below
• Gödels Proofs by Sebastian Bader on 25. Apr. 2006, 14:50
  The talk will focus on the proofs of Gödels incompleteness theorems which state:

  • For any consistent formal theory that proves basic arithmetical truths, it is possible to construct an arithmetical statement that is true but not provable in the theory.
  • For any formal theory that proves basic arithmetical truths, a statement of its own consistency can be proven if and only if it is inconsistent.

  The proofs will be presented in some detail, similar to their original versions.
• The Henhouse Project (II) by Tobias Pietzsch and Stephan Saalfeld on 02. May. 2006, 14:50
  During the last semester, the participants of our workshop "Interaction in Robotic Arts and Artificial Worlds" designed and implemented an interactive installation called "Hühnerstall" (The Henhouse). Aeamer mounted on the ceiling, projects artificial chickens onto the floor. At the same time, a camera registers objects on the playground, enabling human players to interact with the projected world in a very direct way.
  In this talk, we will give an overview of the project and the various problems that had to be solved to create an integrated system. In particular, we will focus on three main components of the system:

  1. tracking people on the playground,
  2. calibrating the camera/beamer setup, and
  3. modeling an appropriate chicken behaviour.

  We will also demonstrate the system as it is currently implemented and discuss possible improvements.
• Efficient symbolic reasoning for FOMDPs: Graph Context versus Object Context by Olga Skvortsova on 09. May. 2006, 14:50
  see below
• Efficient symbolic reasoning for FOMDPs: Graph Context versus Object Context (II) by Olga Skvortsova on 11. May. 2006, 13:00
  First-Order Markov Decision Processes (FOMDPs) have been recently adapted as a representational and computational model for probabilistic planning tasks. In quest of an optimized solution for FOMDPs, it is crucial to reason in first-order terms without descending to the propositional level, especially in cases, where domain is incomplete or infinite. In this talk, we present two modern approaches, referred to as graph context and object context, for performing efficient symbolic reasoning in FOMDPs. In particular, we provide criteria under which one of these is preferred against the other.
• Towards Reliable Component Software: Light-weight Formalism by Ade Azurat on 16. May. 2006, 13:15
  The component software technology is a promising trend for rapid software development. However, one of the main problem of software engineering is inherited, which is the high cost of program verification. Moreover, not just the component, but also the composition of components is a subject for verification. A well defined formal foundation on component framework is required to solve it. We introduce a formal light weight framework to analyse and verify the use of software component. We define some agreements on developing the component and its composition within a framework. By obeying those agreements, we argue that the verification cost, especially on progress property can be reduced. Some theorems that provide the judgement of those agreements are described. We first discuss how the underlying formalism is developed based on a variant of UNITY logic. To justify the soundness, we embed the logic in HOL theorem prover. A quick overview about UNITY logic will also be presented.
• Extending GraphContext for multisets by Georg Rammé on 16. May. 2006, 14:50
  First-Order Markow Decision Processes (FOMDPs) are a novel representational and computational model for probabilistic planning tasks. Many existing implementation perform grounding on the states which is impracticable if the object domain grows. In this talk we will present and extend a method called GraphContext for performing efficient symbolic reasoning in FOMDPs. GraphContext is an algorithm that uses the context information of a term to prune the search space. The context of a term is given by occurences of identical variables. In fact, a term t need not be matched with a term u if the context of t is not embedded in the context of u. We will extend this idea to support multiple occurences of same terms in a state.
• Deepest of the Deep Inference by Ozan Kahramanogullari on 23. May. 2006, 14:50
  The deep inference feature of the calculus of structures causes greater nondeterminism in proof search while providing shorter proofs than in the sequent calculus. We have seen that, by means of conditions that exploit an interaction schema on the structures, deep inference rules can be redesigned in such a way that reduces nondeterminism without losing the shorter proofs. However, when these interaction rules are applied during proof search to structures of arbitrary size, performing the check of the condition (resembling occurs-check of Prolog interpreters) of the interaction rules becomes computationally expensive. In this talk, we will present a general conjecture on the completeness of the calculus of structures systems where inference rules are allowed only at the "deepest" positions. Because deepest instances of the inference rules are applied on the smaller substructures, the check of the condition of the interaction rules is performed only on these smaller structures.
• Reasoning with Programs of Finite Level by Natalia Cherchago on 30. May. 2006, 13:15
  It is well-known that consequences under well-founded semantics (WFS) for normal logic programs are not even semi-decidable. This is a major drawback of all existing ASP approaches that use WFS to approximate answer sets. We attack the problem by introducing a subclass of normal logic programs under WFS called programs of finite level. These programs admit function symbols (hence infinite domains) and still enjoy decidability of query evaluation.
• Genetic Programming and its use for learning Description Logics by Jens Lehmann on 30. May. 2006, 14:50
  Genetic Programming is a Machine Learning technique, which has been succesfully used in various application areas. It is an automated method for creating a program from a problem description. The talk gives an introduction to Genetic Programming and then shows how it can be used to learn Description Logics (in particular ALC).
• Text mining and Web Intelligence Services by Dr. Chunping Li on 13. Jun. 2006, 14:50
  Different from structured data mining, the data set of text clustering and classifying are text objects with semi-structure or non-structure and have sparse data spaces. According to this especial characteristic, we try to find the semantic correlation of text objects in the different stages of the clustering and classifying process and use this correlation to improve the text mining effects.
  In the preprocess of text objects, current existing document representation systems are typically the bag-of-words model, where single word and word stem are used as features for representing document content. In order to strengthen the discriminative feature of text objects, we propose a novel document representation, i.e., Concept Chain Model. On this basis, hierarchical clustering and classfying algorithms process in different levels of concept chains.
  In the definition of text objects, current existing methods of text mining use symmetry smilarity or dissimilarity to measure the correlation of documents. We propose an approach, which uses asymmetric similarity for text mining. Our approach provides a concept structure after the hierarchical text clustering and classifying. Based on our technique, we implement a text mining tool to support for the application on Web intelligence services.
  Please note that this talk will be given in german.
• International Conference on Automated Reasoning and Scheduling (ICAPS) 2006: Flashback by Olga Skvortsova on 20. Jun. 2006, 14:50
  In this talk, I will report on the most interesting papers from the last ICAPS conference that took place in June this year in the beautiful English Lakes District. Moreover, I will give some personal (someone else might have another) impressions about the current state of affairs in the field of planning and which directions of research are currently, from my point of view, the most interesting and promising ones.
• The Fuzzy Linguistic Description Logic ALC_{FL} by Dung Dinh Khac on 27. Jun. 2006, 14:50
  We present the fuzzy linguistic description logic ALC_{FL}, an instance of the description logic framework ALC_L with the certainty lattice characterized by a hedge algebra. Beside constructors of ALC_L, ALC_{FL} allows the modification by hedges. Furthermore, a tableau algorithm for the satisfiability problem in ALC_{FL} is also presented.
• An implementation of fuzzy OWL by Yining Wu on 04. Jul. 2006, 13:15
  Description Logics (DLs) are the basis of the web ontology language OWL. But DLs are limited to dealing with the problem which is either an individual is an instance of a concept or not. In real world, the answers of this kind of questions are not only yes or no. In this project we consider Description Logics with a well-known fuzzy extension to deal with vague information. The topic is to present an implementation of transformation of fuzzy OWL into OWL. I will take a quick look to DLs and fuzzy DLs, and introduce OWL and KAON2, then illustrate the transformation.
• Towards an Implementation of the Neural Symbolic Learning Cycle: A Decompositional Extraction by Valentin Mayer-Eichberger on 04. Jul. 2006, 14:50
  I am currently working on the implementation of a neural symbolic learning cycle. The general idea is to integrate neural networks with logic programs. In particular, I try to do this in the propositional case with main emphasis on the extraction algorithm based on results of my bachelor thesis.
  In this talk I will give a short introduction into the field and present recent results and problems of my approach. The main part is about the decompositional extraction algorithm which means the extraction is done on subnetworks rather than on the network as a whole.
  If you listened to the defence talk of my bachelor thesis from last term, you are still encouraged to come. There will be some parallels, however this presentation will be different in its focus.
• The Design and Implementation of the GraPE (Graphical Proof Editor) by Max Schäfer on 11. Jul. 2006, 14:50
  see below
• The Design and Implementation of the GraPE (Graphical Proof Editor) by Max Schäfer on 14. Jul. 2006, 14:00
  We present GraPE, a graphical proof editor that strives to provide a unified point-and-click interface for a variety of existing theorem provers, and supports advanced proof editing features. It strictly separates the graphical user interface responsible for displaying the derivation being worked on from the actual proof engine, yielding a flexible and powerful theorem proving environment. Unlike many other proof editors, GraPE not only supports inference rules for incrementally building derivations, but also more complex proof generation and manipulation operations, such as automatic proof search and elimination of admissible rules. GraPE provides particularly strong support for the calculus of structures and for integration with the Maude language. We show how this support can be leveraged to quickly and easily obtain a graphical theorem prover for system KSg for classical propositional logic.
  Please note that this talk will be given in room GRU 357.