February 2nd, 2010 | 
Author: Reasoning in Description Logics
Teacher : Anni Turhan (TUD)
Description Logics are a successful family of logic-based knowledge representation formalisms, which can be used to represent the conceptual knowledge of an application domain in a structured and formally well-understood way. Description Logics are closely related to modal and dynamic logics.
Based on the formal semantics, many reasoning procedures have been defined and algorithms to compute them have been investigated for a range of Description Logics. Ontology languages for the emerging Semantic Web such as the OWL dialects have greatly increased interest in Description Logics and related reasoning techniques in recent years, since these ontology languages are based on expressive Description Logics.
Our course gives an introduction to the basic principles underlying knowledge representation with Description Logics. The main focus of the course is on reasoning procedures for Description Logics, which are the core of practical applications of Description Logic systems.
CV:
Anni-Yasmin Turhan is a teaching and research fellow at TU Dresden. She received her Ph.D. in Computer Science from TU Dresden in 2007. She has worked as a research assistant in several research projects dedicated to reasoning in Description Logics – some of them industry funded. Her research interests include knowledge representation and in particular Description Logics. Most of her publications are dedicated to non-standard inferences in DLs and implementations of DL reasoning systems. Anni-Yasmin Turhan has been in the program committee of the international conferences: AAAI’08, IJCAI’09 and ISWC’09. She served as a reviewer for many conferences and workshops in the field of artificial intelligence and logic-based knowledge representation. In 2007 she was a co-PC chair and in 2008 a local organizer of the international Description Logics Workshop.
SAT Solving
Teacher: Steffen Hölldobler(TUD)
The satisfiability or SAT-problem is the standard combinatorial search problem in Computer Science and its applications. In the last decade SAT-solvers have been considerably improved and can now handle problems with millions of variables and clauses. These solvers are able to tackle real world problems in many different domains and are thus an important tool for many applications.
In the first part of the course we introduce the satisfiability or SAT-problem and present various methods for solving it based on systematic search and stochastic local search. In the second part we discuss various applications of SAT-solving in such domains as bioinformatics and termination analysis. In the third part we give an in-depth introduction into modern, state-of-the-art SAT solvers including techniques like watcher lists, backjumping as well as clause learning, and we discuss different heuristics needed in such a system. In the final part, we ask our participants to take an off-the-shelf SAT solver and apply it to examples from Sudoku solving.
CV:
Steffen Hoelldobler is a professor for Knowledge Representation and Reasoning at the TUD since 1993. He is currently Director of the ICCL and co-ordinator of the international MSc. program in Computational Logic as well as the European Master’s Program in Computational Logic. He received his Dr.rer.nat. from the University of the Armed Forces Munich in 1988 and his Habilitation from the Technical University of Darmstadt in 1993. His research interests include logic and logic programming, knowledge representation and reasoning, and connectionist systems. e is the author of four monographs and more than 80 scientific articles.
Interactive Theorem Proving: Program and System Development
Teacher: Michael Posegga (TUD)
In a type-theoretic setting programs can be understood as computable functions between appropriate types and systems are functions defined on process types. Due to the Curry-Howard-Isomorphism it is possible to extract a program from a proof of a corresponding theorem. This can be done also for systems.
New theorem provers combine program and system specification and verification tools and can also be used as a prototype interpreter. The lectures shall give an intentional introduction to these approaches using the concepts of higher-order logic, recursive and corecursive functions and some applications.
CV:
Michael Posegga received his Diploma in Mathematical Logics and Model Theory from the Hunboldt-University Berlin in 1970 and a Dr.rer.nat. for his work on Algebraic Semantics of Model Theory from the same university in 1981. Thereafter he was lecturing at the Humboldt-University Berlin for many years. Since 1988 he is a Scientific Assistant at the TUD. In 1989 he received his Habilitation for his work on Algebraic Type Theories and Category Theory. Since then he lectures on several topics of Theoretical Foundations of Computer Science, Logics, and Interactive Theorem Proving.
A Coalgebraic Approach to Modal Logics
Teacher: Horst Reichel (TUD)
Many different modal logics are used and investigated in Computer Science. Examples are Hennessy-Milner Logic, Probabilistic Modal Logic, Coalition Logic, Description Logic and others. As usual a great diversification gives rise to unification. We will demonstrate that coalgebras can be used as a unifying modeltheoretic semantics. In this approach the types of coalgebras serve as parameter for the different coalgebraic modal logics. Coalgebras are suitable mathematical structures to model state-based dynamic systems. This will be demonstrated by several examples. Finally we will show how modal logics can be derived from given types of coalgebras in such a way that two states are logically equivalent if and only if they are bisimilar. The generated logics are decidable in reasonable complexity classes. The coalgebraic approach to modal logics has been developed in the last 10 years and it is an active and interesting research field. The Coalgebraic Logic Satisfiability Solver (CoLoSS) is a first attempt to tool support.
CV:
Horst Reichel received his Ph.D. in Mathematics from the Technische Universität in Dresden in 1968. From 1968-1980 he was a researcher and head of a research department in computer industry. In 1980 he received his habilitation from Humboldt-University Berlin and became a full Professor of Algebra at Technical University of Magdeburg. His research interests include algebraic specification of abstract data types, category theory, partial algebras, behavioral specification of systems, applications of coalgebras in theoretical computer science. From 1987-2006 he was a full professor of algebraic and logical foundations of computer science at the Technische Universitat Dresden. He is a founding member of the IFIP WG1.3 Foundations of System Specification, member of the steering committees of CALCO and CMCS (coalgebraic methods in computer science). He was program chair and member of the program committees of several international conferences. He has published over 60 articles in journals and conferences.
Transforming and Completing Logic Programs
Teacher: Johannes Stefanus (University of Indonesia)
This set of lectures focuses on how to transform logic programs (in order to improve them) in logically defensible ways, such as the techniques of unfolding and folding. The logical justification of these techniques requires reference not only to the explicit contents of the programs but also to their implicit contents under the closed-world assumption. This assumption can be formalized through the operation of program completion, which is elaborated in this course in relation to default reasoning.
CV:
Yohanes Stefanus received a Ph.D. in Computer Science from the University of Waterloo, Waterloo, Canada in 1992. He is currently a lecturer in the Faculty of Computer Science at the University of Indonesia, Depok/Jakarta. In the winter term 2004/5 and the spring term 2008 he was a visiting professor at the Computer Science Department of TUD, Germany. In the spring term 2009 he was a visiting professor at the Computer Science Department of UNL, Portugal. His research interests include Algebraic Computing, Computer-Aided Geometric Design and Formal Methods in Software Engineering.
XSTL and Logic Programming
Teacher: Josef Schneeberger (FH Deggendorf)
CV:
Josef Schneeberger studied computer science at the Technical Universities in Munich and Darmstadt (Germany). He also worked at the Universities in Munich and Darmstadt as a researcher on export systems and AI planning. He received his Ph.D. in 1992 for a novel method on deductive planning. Subsequently he was the leader of a research group at the Bavarian Research Center for Knowledge Based Systems (FORWISS) in Erlangen. 1996 he joined the newly founded SCHEMA Inc. in Nuremberg as a partner. Until now SCHEMA grew to the size of 65 employees and became a leading software manufacturer for innovative documentation and content management solutions. Since November 2002 Josef Schneeberger is also a Professor for software and Internet technology at the University of Applied Sciences in Deggendorf. He works and lectures in the areas of knowledge based systems, knowledge management, software agents, agent oriented programming, information logistics and documentation technology based on XML.
Projection Computation
Teacher: Christoph Wernhard (TUM)
Projection computation provides a semantically founded view on extracting the knowledge about a given set of concepts from a given knowledge base. Variants of projection computation are also known as forgetting, second-order quantifier elimination, Boolean quantifier elimination, and computation of uniform interpolants. In this course, we develop a semantic characterization of projection for first-order logic and relate variants from the literature to it. We survey methods for projection computation – or the closely related elimination of second-order quantifiers. The two prevalent approaches are resolvent generation (the SCAN algorithm) and formula rewriting with the Ackermann lemma (the DLS algorithm). Further recent approaches are based on tableau construction, knowledge compilation, answer set computation and description logic reasoning. A large variety of tasks in knowledge processing can be expressed with projection computation. For example, abduction, knowledge base modularization, extraction of relevant knowledge and specializing compiled knowledge bases. In addition, there are strong relationships between projection computation and non-monotonic reasoning. In the course, we devise patterns for the application of projection computation to such tasks.
CV:
ChristophWernhard is a research and teaching assistant at TU Dresden. He received his Dr. rer. Nat. in Computer Science from University Koblenz-Landau in 2008. He worked as a research assistant in several university projects related to automated deduction and as a senior developer in a Semantic Web company. His research interests include theoretical and practical aspects of logic-based knowledge representation.
Posted in Summer School