SummerSchool2015/en

• Info
• Lecturers and Lectures

In September 2015 we organize a summer school, which will be held before the German AI conference. The conference and the summer school will be coupled.

The web pages for this summer school are under construction.

Term Rewriting Systems (6h) by Franz Baader (Technische Universität Dresden, Germany)

Term rewriting is an important branch of theoretical computer science which combines elements of logic and mathematics. In fact, term rewriting systems can be used to compute in structures that are defined by equations. They are thus an important tool in automated deduction, algebraic specification, and functional programming. The course introduces important properties such as termination and confluence of term rewriting systems, shows methods for checking termination and confluence, and finally describes how Knuth-Bendix completion can (sometimes) be used to make non-confluent term rewriting systems confluent.

Model Checking (4h) by Christel Baier (Technische Universität Dresden, Germany)

Markov chains (MC) and Markov decision processes (MDP) are widely used as operational models for the quantitative system analysis. They can be understood as transition systems augmented with distributions for the states (in MC) or state-action pairs (in MDPs) to specify the probabilities for the successor states. Additionally one might add weight functions for modeling accumulated costs or rewards earned along path fragments to represent e.g. the energy consumption, the penality to be paid for missed deadlines, the gain for completing tasks successfully or the degree of the achieved utility. The tutorial will introduce the main features of discrete-time, finite-state Markovian models (MC and MDP) and their quantitative analysis against temporal logic specifications. The first part will present the basic princi- ples of the automata-based approach for linear temporal logic (LTL) and probabilistic computation tree logic (PCTL), including a summary of techniques that have been proposed to tackle the state-explosion problem. The second part of the tutorial will present algorithms for dealing with fairness assumptions and computing conditional probabilities and quantiles

Human Reasoning (6h) by Emmanuelle Dietz, Steffen Hölldobler, Marco Ragni (Technische Universität Dresden, Albert-Ludwigs Universität Freiburg, Germany)

Recently, the lecturers have introduced a new approach to model human reasoning based on logic programming employing as techniques model generation, weak completion semantics and abduction under the three-valued Lukasiewicz logic. In the course we will present the approach in detail, discuss its relation to well-founded semantics, and show how it can be applied to model important phenomena of human reasoning such as the suppression and the selection task as well as the belief-bias effect. We discuss novel extensions of abduction and present a connectionist realization.

Abstract Argumentation – Reasoning, Expressiveness and its Connection to Answer Set Programming (6h) by Sarah Alice Gaggl (Technische Universität Dresden, Germany)

Argumentation is one of the major fields in Artificial Intelligence (AI) and Non-Monotonic Reasoning (NMR). Nowadays, the concept of Abstract Argumentation Frameworks (AFs) is one of the most popular approaches to capture certain aspects of argumentation. This very simple yet expressive model has been introduced by Phan Minh Dung in 1995. Arguments and a binary “attack” relation between them, denoting conflicts, are the only components one needs for the representation of a wide range of problems and the reasoning therein. Nowadays numerous semantics exist to solve the inherent conflicts between the arguments by selecting sets of “acceptable” arguments. Depending on the application, acceptability is defined in different ways. Some semantics are based on the idea to defend arguments against attacks, while others treat arguments like different choices and the solutions stand for consistent sets of arguments. In this course we will first focus on the expressiveness of AFs, in particular we will study if, and under which conditions, a given set of arguments can be accepted at all in an AF under a given semantics. Furthermore, we will analyze different notions of equivalences for AFs, for example when two different AFs posses the same solutions under a semantics, even if we apply modifications to them. Finally we will observe the connection between answer set programming (ASP) and AFs.

SAT Solving (6h) by Steffen Hölldobler, Norbert Manthey (Technische Universität Dresden, Germany)

Satisfiability testing (SAT) is applied in a wide range of applications, for example hardware model checking, planning, periodic event scheduling or bio informatics. The reason for solving many combinatorial problems with the same reasoning system is the strength of the so-called SAT solvers that have been improved significantly about two decades ago and received much attention afterwards. This course briefly introduces why modern SAT solvers are so strong and de- tails some of the significant contributions in the area. The main focus of the course is the discussion of techniques that improved the solvers. Additionally, propositional proof theory is related to modern solvers, and the solvers major deduction technique resolution will be discussed in more detail, because the power of the solvers relies on the reasoning power. Finally, an overview on related applications is given to introduce ways how SAT solvers can be used to solve combinatorial problems.

OWL 2 Profiles: An Introduction to Lightweight Ontology Languages (4h) by Markus Krötzsch (Technische Universität Dresden, Germany)

This course gives an extended introduction to the lightweight profiles OWL EL, OWL QL, and OWL RL of the Web Ontology Language OWL. The three ontology language standards are sublanguages of OWL DL that are restricted in ways that significantly simplify ontological reasoning. Compared to OWL DL as a whole, reasoning algorithms for the OWL profiles show higher performance, are easier to implement, and can scale to larger amounts of data. Since ontological reasoning is of great importance for designing and deploying OWL ontologies, the profiles are highly attractive for many applications. These advantages come at a price: various modelling features of OWL are not available in all or some of the OWL profiles. Moreover, the profiles are mutually incomparable in the sense that each of them offers a combination of features that is available in none of the others. This chapter provides an overview of these differences and explains why some of them are essential to retain the desired properties. To this end, we recall the relationship between OWL and description logics (DLs), and show how each of the profiles is typically treated in reasoning algorithms.

Query Answering under Existential Rules (2h) by Sebastian Rudolph (Technische Universität Dresden, Germany)

The course focuses on a problem called ontological query answering, which consists in querying data while taking general domain knowledge (an ontology) into account. The ontology is assumed to be expressed via a set of existential rules (which have been known under many different names like tuple-generating dependencies, Datalog+/-, and forall-exists-rules). As the general problem is undecidable, restrictions need to be imposed to guarantee decidability. Over the last years, a lot of ever more expressive such decidable existential rule fragments have been identified. We will provide an overview of these fragments, relate them to general priciples of decidability, and discuss the different algorithmic approaches to query answering that they give rise to.

Answer Set Programming (6h) by Torsten Schaub (Universität Potsdam, Germany)

The tutorial aims at acquainting the participant with ASP’s modeling and solving methodology, enabling her/him to independent problem solving using ASP systems. To this end, the tutorial starts with an introduction to the essential formal concepts of ASP, needed for understanding its semantics and solving technology. In fact, ASP solving rests on two major components: A grounder turning specifications in ASP’s modeling language into propositional logic programs and a solver computing a requested number of answer sets of the given program. Building on the aforementioned formal concepts, we provide a characterization of ASP’s inference schemes that are in turn mapped into algorithms relying on advanced Boolean Constraint technology. We illustrate this technology through the ASP solver clasp, developed at the University of Potsdam, and winning first places at international ASP, CASC, MISC, PB, and SAT competitions. Similarly, ASP’s grounding inferences are discussed in conjunction with (deductive) database techniques. The remainder of the tutorial is dedicated to applying ASP, involving an introduction to ASP’s modeling language, its solving methodology, and advanced techniques fostering scalability. The latter is illustrated via some real-world applications, taken from bio-informatics.