International Center for Computational Logic - Benutzerbeiträge [de]

Techreport3031

2018-06-22T09:02:48Z

Norbert Manthey:

{{Publikation Erster Autor
|ErsterAutorVorname=Norbert
|ErsterAutorNachname=Manthey
}}
{{Techreport
|Title=An A-Maze-ing SAT Solving Visualization
|Year=2015
|Month=April
|Institution=TU Dresden
}}
{{Publikation Details
|Bild=Sat-maze-nmanthey-2015.pdf
|Download=Sat-maze-nmanthey-2015.pdf
|Projekt=PSAT
|Forschungsgruppe=Wissensverarbeitung
}}

Techreport3030

2017-05-04T20:05:37Z

Norbert Manthey:

{{Publikation Erster Autor
|ErsterAutorVorname=Norbert
|ErsterAutorNachname=Manthey
}}
{{Techreport
|Title=Refining Unsatisfiable Cores in Incremental SAT Solving
|Year=2015
|Month=September
|Institution=TU Dresden
}}
{{Publikation Details
|Bild=Refine-cores-nmanthey-2015.pdf
|Download=Refine-cores-nmanthey-2015.pdf
|Projekt=PSAT
|Forschungsgruppe=Wissensverarbeitung
}}

Techreport3031/en

2017-05-04T19:49:48Z

Norbert Manthey: Page created automatically by parser function on page Techreport3031

#REDIRECT [[Techreport3031]]

Techreport3031

2017-05-04T19:49:48Z

Norbert Manthey: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Norbert |ErsterAutorNachname=Manthey }} {{Techreport |Title=An A-Maze-ing SAT Solving Visualization |Year=2015 |…“

{{Publikation Erster Autor
|ErsterAutorVorname=Norbert
|ErsterAutorNachname=Manthey
}}
{{Techreport
|Title=An A-Maze-ing SAT Solving Visualization
|Year=2015
|Month=April
|Institution=TU Dresden
}}
{{Publikation Details
|Bild=Sat-maze-nmanthey-2015.pdf
|Projekt=PSAT
|Forschungsgruppe=Wissensverarbeitung
}}

Datei:Sat-maze-nmanthey-2015.pdf

2017-05-04T19:48:22Z

Norbert Manthey:

Techreport3030

2017-05-04T19:45:24Z

Norbert Manthey: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Norbert |ErsterAutorNachname=Manthey }} {{Techreport |Title=Refining Unsatisfiable Cores in Incremental SAT Solv…“

{{Publikation Erster Autor
|ErsterAutorVorname=Norbert
|ErsterAutorNachname=Manthey
}}
{{Techreport
|Title=Refining Unsatisfiable Cores in Incremental SAT Solving
|Year=2015
|Month=September
|Institution=TU Dresden
}}
{{Publikation Details
|Bild=Refine-cores-nmanthey-2015.pdf
|Projekt=PSAT
|Forschungsgruppe=Wissensverarbeitung
}}

Datei:Refine-cores-nmanthey-2015.pdf

2017-05-04T19:42:52Z

Norbert Manthey: Article that describes how incremental SAT solving could be improved

Article that describes how incremental SAT solving could be improved

News21/en

2015-10-09T06:42:38Z

Norbert Manthey: Page created automatically by parser function on page News21

News21

2015-10-09T06:42:36Z

Norbert Manthey: Die Seite wurde neu angelegt: „{{Neuigkeit |Titel DE=Mitarbeiter der Wissensverarbeitung entwickeln Weltspitze-Werkzeuge für Generische Problemlöser |Titel EN=Tools of the ICCL have receiv…“

{{Neuigkeit
|Titel DE=Mitarbeiter der Wissensverarbeitung entwickeln Weltspitze-Werkzeuge für Generische Problemlöser
|Titel EN=Tools of the ICCL have received first prizes in several international competitions
|Beschreibung DE=Im Zeitalter der Automatisierung müssen immer komplexerer Systeme in immer kürzerer Zeit viel mehr Aufgaben lösen. Die Forschung beschäftigt sich daher seit einiger Zeit mit der Entwicklung möglichst effizienter Verfahren (sogenannter SAT-Solver), um die Zuverlässigkeit und Korrektheit von Programmen und Geräten zu garantieren. SAT Solver helfen beispielsweise beim Überprüfen eines Computersystems auf Fehler, beim Erstellen eines guten Fahrplans, den Betriebsablauf in einer Fabrik zu optimieren, Programmfehler in Software oder fehlerhafte Zustände in Schaltkreisentwürfen zu finden. Dazu überprüfen sie riesige Systembeschreibungen und bestimmen die Voraussetzungen, unter denen das jeweilige System fehlerfrei arbeitet oder zeigen einen konkreten Fehler auf.

An der Fakultät Informatik der TU Dresden entwickelt [[Norbert Manthey]] an der Professur für [[Wissensverarbeitung]] seit fünf Jahren den SAT Solver „[[Riss]]“ und gemeinsam mit Studenten darauf aufbauende Werkzeuge. Diese Forschung wird inzwischen durch ein DFG Projekt gefördert. In den diesjährigen internationalen SAT-Wettbewerben für Hardware Model Checking, der MaxSAT Evaluation sowie der SAT Race hat die Gruppe gezeigt, dass die entwickelten Werkzeuge in allen drei Bereichen an der Weltspitze agieren. Norbert Manthey freut sich über den Erfolg: "Es macht uns stolz, dass wir in immer mehr Bereichen weltweit wettbewerbsfähig werden und an die Vorjahreserfolg anknüpfen können.“ Die Ziele der drei Wettbewerbe decken wesentliche Anwendungsgebiete der SAT-Solver ab: Die Hardware Model Checking Competition vergleicht, wie gut Systemprüfer, sogenannte Modelchecker, beweisen können, ob ein Schaltkreis einen fehlerhaften Zustand erreichen kann oder nicht. Ein besonderes Augenmerk liegt auf nicht komplett beweisbare Schaltkreise - hier versucht man zu zeigen, dass der fehlerhafte Zustand möglichst lange nicht auftritt. In dieser Kategorie hat das von Manthey entwickelte Werkzeug „ShiftBMC“ den ersten Platz belegen können, welcher mit einem 500 USD Preisgeld der Firma Oski Technology dotiert wurde.
In der SAT Race werden Lösungen für industrielle kombinatorische Probleme gesucht und entsprechende Werkzeuge miteinander verglichen. Besonders bedeutsam ist hier das Anpassen an die wechselnden Problemkombinationen, da die Zahl der Anwendungsgebiete, von Jahr zu Jahr steigt. Der SAT Solver „Riss“ konnte hier einen dritten Platz belegen.
In der MaxSAT Evaluierung werden optimale Lösungen von diskrete Optimierungsprobleme gesucht. Dabei gibt es zwei unterschiedliche Kategorien: das Beweisen einer optimalen Lösung mit relativ viel Zeit oder das Auffinden einer möglichst guten Lösung innerhalb von zehn Minuten. Für Optimierungsaufgaben aus der Industrie konnte das Werkzeug „Optiriss“ in der zweiten Kategorie erste zweite und dritte Plätze belegen, je nach Beschaffenheit der Optimierungsaufgaben.
Ein Grund für das gute Abschneiden der Systeme ist unter anderem auch der dieses Jahr eingeweihte Hochleistungsrechner der TU Dresden, durch den Auswertungszeiten wesentlich verkürzt werden.
|Beschreibung EN=In the era of Industry 4.0 and automation more and more combinatorial tasks have to be solved automatically, and hence actual systems become more complex as well.
Hence, research focusses on efficient decision procedures - here so called SAT solvers - that can be used to show that correctness and reliability of the use programs and machines.
SAT solvers can be used for example to check circuits for faulty states, to create good rail ways schedules, to optimize the workflow in manufactories or to find bugs in software systems.
For these tasks, a SAT solvers is given a huge specification for which it either states that the system works correctly, or it points out a specific case of misbehavior.

The SAT solver "Riss" is developped by [[Norbert Manthey]] in the knowledge representation and reasoning group for 5 years now, where student projects are also integrated into the system or related software packages. In three SAT related international competitions, which cover major application areas of SAT solver, the group showed that it is quite competitive on an international level. The good results live up to the success of the previous years.

In the hardware model checking competition model checkers have to prove correctness of a circuit or have show a counter example for this correctness.
For circuits that are to difficult to be proven, there is another track: showing that a faulty state cannot be reached as long as possible.
This track has been won by the model checker "ShiftBMC" of the group.

In the SAT Race, this years version of the bi-yearly SAT competition with moderate timeouts and a focus on industrial problems.
An important feature of a succesful system is to be able to adapt to the given problem, as the number of applications for SAT solvers increases every years.
In this competition, the SAT solver "Riss" achieved a third place.

The MaxSAT competition searches for optimal solutions for discrete optimization problems with two different categories: either, withing a rather long timeout the optimality of the solution has to be proven by showing that no better solution exists, or, within a small timeout of 10 minutes a very good solution has to be reported without the optimality proof.
For industrial problems in the latter category the MaxSAT solver "Optiriss" has been awarded first, second and third, depending on the actual kind of the optimization problem.
|Datum=2015/10/09
|Bild=Norbert.jpg
|Forschungsgruppe=Wissensverarbeitung
}}

Soft Skills Lectures

2015-10-06T08:51:01Z

Norbert Manthey:

== Slides ==
* How to give a research talk – Emmanuelle Dietz
* [http://www.wv.inf.tu-dresden.de/~wernhard/teaching/writing2015.pdf How to write a research paper – Christoph Wernhard]
* [https://ddll.inf.tu-dresden.de/w/images/6/65/LatexIntro.pdf Introduction to LaTeX – Peter Steinke]
* Introduction to Beamer – Tobias Philipp
* Introduction to [https://ddll.inf.tu-dresden.de/w/images/4/4a/Tikz-introduction-2015.pdf TikZ] and [https://ddll.inf.tu-dresden.de/w/images/0/0f/Git-introduction-2015.pdf GIT] – Norbert Manthey

Datei:Git-introduction-2015.pdf

2015-10-06T08:50:32Z

Norbert Manthey:

Datei:Tikz-introduction-2015.pdf

2015-10-06T08:49:14Z

Norbert Manthey:

Article3015/en

2015-09-15T07:11:01Z

Norbert Manthey: Page created automatically by parser function on page Article3015

#REDIRECT [[Article3015]]

Article3015

2015-09-15T07:10:58Z

Norbert Manthey: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Norbert |ErsterAutorNachname=Manthey }} {{Article |Referiert=1 |Title=Towards next generation sequential and par…“

{{Publikation Erster Autor
|ErsterAutorVorname=Norbert
|ErsterAutorNachname=Manthey
}}
{{Article
|Referiert=1
|Title=Towards next generation sequential and parallel SAT solvers
|To appear=0
|Year=2015
|Month=September
|Journal=Constraints
|Pages=1-2
|Publisher=Springer US
}}
{{Publikation Details
|ISSN=1383-7133
|Link=http://dx.doi.org/10.1007/s10601-015-9226-6
|DOI Name=10.1007/s10601-015-9226-6
|Forschungsgruppe=Wissensverarbeitung
}}

SAT-Solving und das Lösen von Sudokus (SS2015)

2015-07-25T12:09:44Z

Norbert Manthey:

{{Vorlesung
|Title=SAT-Solving
|Research group=Wissensverarbeitung
|Lecturers=Steffen Hölldobler;Norbert Manthey;
|Tutors=Peter Steinke;
|Term=SS
|Year=2015
|Module=INF-PM-FOR, INF-VERT2, MCL-KR, MCL-PI
|SWSLecture=2
|SWSExercise=2
|SWSPractical=0
|Exam type=mündliche Prüfung
|Description=Vorlesung: Montag, 4. DS Übung: Montag, 5. DS

Die Vorlesung beginnt immer 13:15 und endet dafür 14:45 Uhr 

Das Erfüllbarkeitsproblem (SAT) der Aussagenlogik ist ein fundamentales Entscheidungsproblem der Informatik, und das repräsentative Problem der Komplexitätsklasse NP. Neben vielen akademischen Anwendungen, die sich auf SAT reduzieren lassen, gibt es auch industriell relevante Probleme, die gelöst werden können. Einige Beispiele sind das Lösen von Sudokus, das Lösen von Hamiltonion Path und Hamiltonian Cycle Problemen, aber auch die Verifikation von Hardware und Software. Selbst Attacken auf Crypthographie-Verfahren sind mit SAT möglich.

In den letzten zwei Jahrzehnten wurden SAT Solver -- Algorithmen die das Efüllbarkeitsproblem lösen -- wesentlich verbessert, und gehen weit über den DPLL Algorithmus der 1960er hinaus. Die Vorlesung präsentiert zum einen die theoretischen Grundlagen, auf denen SAT Solver aufbauen und führt Lösungsalgorithmen abstrakt ein und diskutiert Eigenschaften, die ausgenutzt werden können, um effiziente SAT Solver zu erhalten.

Auf der anderen Seite werden interna von SAT Solvern beleuchtet, und verwandte Anwendungen aufgezeigt. So kann mit MaxSAT -- der Optimierungsvariante des Erfüllbarkeitsproblems -- eine beste Lösung gefunden werden, oder durch mehrfaches Aufrufen eines Solvers eine kleinste unerfüllbare Teilformel gefunden werden. Die Varianten des Lösens werden ebenso diskutiert, wie das parallele Lösen des SAT Problems. Dabei wird auch auf die effiziente Implementierung geachtet.

In den Übungen werden sowohl theoretische als auch praktische Aufgabenstellungen gegeben. Es sollen sowohl Lösungsalgrithmen implementiert, als auch Probleme auf das SAT Problem reduziert werden.
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Exercise 1
|Room=APB E005
|Date=2015/04/20
|DS=DS5
|Download=Exercise 1.pdf,
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Exercise 2
|Room=APB E005
|Date=2015/04/27
|DS=DS5
|Download=Exercise 2.pdf,
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=SAT Problems
|Room=APB E005
|Date=2015/04/20
|DS=DS5
|Download=Satproblems2015.pdf,
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=SAT Introduction
|Room=APB E005
|Date=2015/04/13
|DS=DS5
|Download=Introduction2015.pdf,
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Exercise 3
|Room=APB E005
|Date=2015/05/04
|DS=DS5
|Download=Exercise 3.pdf,
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Systematic Search
|Room=APB E005
|Date=2015/05/04
|DS=DS4
|Download=Systematic2015.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Exercise 4
|Room=APB E005
|Date=2015/06/01
|DS=DS5
|Download=Exercise 4.pdf,
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Stochastic Local Search
|Room=APB E005
|Date=2015/06/08
|DS=DS4
|Download=Sls2015.pdf,
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Exercise 5
|Room=APB E005
|Date=2015/06/08
|DS=DS5
|Download=Exercise 5.pdf,
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=SAT Algorithms
|Room=APB E005
|Date=2015/06/15
|DS=DS4
|Download=SAT-Solving-Algorithms2015.pdf,
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=SAT - Programming
|Room=APB E005
|Date=2015/06/22
|DS=DS4
|Download=SAT2015-Programming.pdf,
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=CNF Benchmark
|Room=APB E005
|Date=2015/06/29
|DS=DS5
|Download=Sudoku cnfs.zip,
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Konflikt Analyse
|Room=APB E005
|Date=2015/06/29
|DS=DS4
|Download=SAT2015-ConflictAnalysis-graphs.pdf,
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Simplification
|Room=APB E005
|Date=2015/07/06
|DS=DS4
|Download=SAT2015-Simplification.pdf,
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Parallel SAT Solving
|Room=APB E005
|Date=2015/07/13
|DS=DS4
|Download=SAT2015-ParallelSAT.pdf,
}}

Datei:SAT2015-ParallelSAT.pdf

2015-07-25T12:09:24Z

Norbert Manthey:

Forschungslinie (SS2015)

2015-07-07T09:47:51Z

Norbert Manthey:

{{Vorlesung
|Title=Forschungslinie
|Research group=Wissensverarbeitung
|Lecturers=Steffen Hölldobler;
|Term=SS
|Year=2015
|SWSLecture=0
|SWSExercise=0
|SWSPractical=0
|Exam type=Hausarbeit
|Description=Diese Vorlesung im Rahmen der Forschungslinien-Vorlesung stellt kurz die Forschung um das Erfüllbarkeitsproblem dar. Weitere Details, auch zu dem damit verbundenen Wettbewerb finden Sie zeitnah auf dieser Webseite.

Wettbewerb 
Es soll ein Löser entwickelt werden, der einen Graphen im DIMACS-Graph-Format einlesen kann, und für diesen Graph einen Hamiltonian-Cycle ausgibt, oder ausgibt, dass es keine Lösung gibt. Im Wettbewerb werden mehrere Graphen gelöst. Der Löser, welcher die meisten Graphen in einem gegebenen Timeout (ca. 10 Minuten) erfolgreich lösen kann, gewinnt. Löser, die eine falsche Lösung ausgeben, werden disqualifiziert. Beispielgraphen gibt es hier: http://mat.gsia.cmu.edu/COLOR/instances.html

Abgabetermin 
Die finale Version des Werkzeugs muss am Freitag, 3.7., bis 24:00 eingereicht worden sein.

Wettbewerbsumgebung 
Unter dem Reiter Termine und Unterlagen wurden Datein für die Wettbewerbungsumgebung und ein Generator für Graphen hinterlegt. Die genutzte Umgebung für den Wettbewerb wird dazu sehr ähnlich sein. Die neuste Version wurde am 30.6. zur Verfügung gestellt.

Format und andere Details 

<ul>
<li>das Format für die Lösung ist (da gibt es ein Checker-Werzeug in der Umgebung geben, was nur dieses Format richtig erkennt, und eure Lösungen entsprechend bewertet):</li>
<ul>
<li>
kein Cycle: 
"s UNSATISFABLE" 
auf stdout, exitcode 20 
</li>
<li>
ein Cycle mit dem Pfad 5->3->4->1->2->5 
"s SATISFIABLE" 
"v 5 3 4 1 2" 
auf stdout, exitcode 10 
</li>
</ul>
<li>
Die Graphen sind eigentlich gerichtet, der Generator liefert für
kleine Graphen meist ungerichtete Graphen, da beide Kanten da sind.
Für größere Graphen ist das nicht garantiert.
</li>
<li>
Der Generator ordnet die Kanten, darauf kann man sich aber nicht
verlassen, falls ich Graphen von außen mit zulasse.
</li>
<li>
Der SAT Solver darf mehrfach aufgerufen werden. Dann interessiert uns was ihr damit genau tut.
</li>
</ul>

Registrierung 
Um an dem Wettbewerb teilnehmen zu können, müssen sich die Team von maximal drei Studenten mit einem Teamnamen, sowie der Namen der Studenten und der Matrikelnummer per Email bis zwei Wochen vor dem Wettbewerb bei Norbert Manthey (Vorname.Nachname at tu-dresden.de) registrieren. Eine Vorabversion des Tools muss bis eine Woche vor dem Wettbewerb eingereicht werden, damit sie auf ihre Lauffähigkeit getestet werden kann (der Wettbewerb wird auf einem Linux System ausgetragen). Der Wettbewerb findet nur statt, wenn sich mindestens drei Teams angemeldet haben.
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Vorstellung der SAT Forschung
|Room=APB E023
|Date=2015/04/13
|DS=DS5
|Download=Satvorstellung-Forschungslinie-SS2015.pdf,Satvorstellung-Forschungslinie-SS2015.pdf,
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Auswertung des Wettbewerbes
|Room=APB E023
|Date=2015/07/06
|DS=DS5
|Download=HamiltonianCycleCompetition-Environment-SS2015.tar.gz,
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Graphen des Wettbewerbs
|Room=APB E023
|Date=2015/07/06
|DS=DS5
|Download=Forschungslinie2015-Graphs.tar.gz,
}}

Forschungslinie (SS2015)

2015-07-07T09:47:27Z

Norbert Manthey:

{{Vorlesung
|Title=Forschungslinie
|Research group=Wissensverarbeitung
|Lecturers=Steffen Hölldobler;
|Term=SS
|Year=2015
|SWSLecture=0
|SWSExercise=0
|SWSPractical=0
|Exam type=Hausarbeit
|Description=Diese Vorlesung im Rahmen der Forschungslinien-Vorlesung stellt kurz die Forschung um das Erfüllbarkeitsproblem dar. Weitere Details, auch zu dem damit verbundenen Wettbewerb finden Sie zeitnah auf dieser Webseite.

Wettbewerb 
Es soll ein Löser entwickelt werden, der einen Graphen im DIMACS-Graph-Format einlesen kann, und für diesen Graph einen Hamiltonian-Cycle ausgibt, oder ausgibt, dass es keine Lösung gibt. Im Wettbewerb werden mehrere Graphen gelöst. Der Löser, welcher die meisten Graphen in einem gegebenen Timeout (ca. 10 Minuten) erfolgreich lösen kann, gewinnt. Löser, die eine falsche Lösung ausgeben, werden disqualifiziert. Beispielgraphen gibt es hier: http://mat.gsia.cmu.edu/COLOR/instances.html

Abgabetermin 
Die finale Version des Werkzeugs muss am Freitag, 3.7., bis 24:00 eingereicht worden sein.

Wettbewerbsumgebung 
Unter dem Reiter Termine und Unterlagen wurden Datein für die Wettbewerbungsumgebung und ein Generator für Graphen hinterlegt. Die genutzte Umgebung für den Wettbewerb wird dazu sehr ähnlich sein. Die neuste Version wurde am 30.6. zur Verfügung gestellt.

Format und andere Details 

<ul>
<li>das Format für die Lösung ist (da gibt es ein Checker-Werzeug in der Umgebung geben, was nur dieses Format richtig erkennt, und eure Lösungen entsprechend bewertet):</li>
<ul>
<li>
kein Cycle: 
"s UNSATISFABLE" 
auf stdout, exitcode 20 
</li>
<li>
ein Cycle mit dem Pfad 5->3->4->1->2->5 
"s SATISFIABLE" 
"v 5 3 4 1 2" 
auf stdout, exitcode 10 
</li>
</ul>
<li>
Die Graphen sind eigentlich gerichtet, der Generator liefert für
kleine Graphen meist ungerichtete Graphen, da beide Kanten da sind.
Für größere Graphen ist das nicht garantiert.
</li>
<li>
Der Generator ordnet die Kanten, darauf kann man sich aber nicht
verlassen, falls ich Graphen von außen mit zulasse.
</li>
<li>
Der SAT Solver darf mehrfach aufgerufen werden. Dann interessiert uns was ihr damit genau tut.
</li>
</ul>

Registrierung 
Um an dem Wettbewerb teilnehmen zu können, müssen sich die Team von maximal drei Studenten mit einem Teamnamen, sowie der Namen der Studenten und der Matrikelnummer per Email bis zwei Wochen vor dem Wettbewerb bei Norbert Manthey (Vorname.Nachname at tu-dresden.de) registrieren. Eine Vorabversion des Tools muss bis eine Woche vor dem Wettbewerb eingereicht werden, damit sie auf ihre Lauffähigkeit getestet werden kann (der Wettbewerb wird auf einem Linux System ausgetragen). Der Wettbewerb findet nur statt, wenn sich mindestens drei Teams angemeldet haben.
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Vorstellung der SAT Forschung
|Room=APB E023
|Date=2015/04/13
|DS=DS5
|Download=Satvorstellung-Forschungslinie-SS2015.pdf,Satvorstellung-Forschungslinie-SS2015.pdf,
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Auswertung des Wettbewerbes
|Room=APB E023
|Date=2015/07/06
|DS=DS5
|Download=HamiltonianCycleCompetition-Environment-SS2015.tar.gz,
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Graphen des Wettbewerbs
|Room=APB E005
|Date=2015/07/06
|DS=DS5
|Download=Forschungslinie2015-Graphs.tar.gz,
}}

Datei:Forschungslinie2015-Graphs.tar.gz

2015-07-07T09:46:51Z

Norbert Manthey:

SAT-Solving und das Lösen von Sudokus (SS2015)

2015-07-07T09:45:30Z

Norbert Manthey:

Datei:SAT2015-Simplification.pdf

2015-07-07T09:43:56Z

Norbert Manthey:

Datei:SAT2015-Programming.pdf

2015-07-07T09:42:57Z

Norbert Manthey:

Datei:SAT2015-ConflictAnalysis-graphs.pdf

2015-07-07T09:41:47Z

Norbert Manthey:

Forschungslinie (SS2015)

2015-06-30T08:45:02Z

Norbert Manthey:

Forschungslinie (SS2015)

2015-06-30T08:43:38Z

Norbert Manthey:

{{Vorlesung
|Title=Forschungslinie
|Research group=Wissensverarbeitung
|Lecturers=Steffen Hölldobler;
|Term=SS
|Year=2015
|SWSLecture=0
|SWSExercise=0
|SWSPractical=0
|Exam type=Hausarbeit
|Description=Diese Vorlesung im Rahmen der Forschungslinien-Vorlesung stellt kurz die Forschung um das Erfüllbarkeitsproblem dar. Weitere Details, auch zu dem damit verbundenen Wettbewerb finden Sie zeitnah auf dieser Webseite.

Wettbewerb 
Es soll ein Löser entwickelt werden, der einen Graphen im DIMACS-Graph-Format einlesen kann, und für diesen Graph einen Hamiltonian-Cycle ausgibt, oder ausgibt, dass es keine Lösung gibt. Im Wettbewerb werden mehrere Graphen gelöst. Der Löser, welcher die meisten Graphen in einem gegebenen Timeout (ca. 10 Minuten) erfolgreich lösen kann, gewinnt. Löser, die eine falsche Lösung ausgeben, werden disqualifiziert. Beispielgraphen gibt es hier: http://mat.gsia.cmu.edu/COLOR/instances.html

Abgabetermin 
Die finale Version des Werkzeugs muss am Freitag, 3.7., bis 24:00 eingereicht worden sein.

Wettbewerbsumgebung 
Unter dem Reiter Termine und Unterlagen wurden Datein für die Wettbewerbungsumgebung und ein Generator für Graphen hinterlegt. Die genutzte Umgebung für den Wettbewerb wird dazu sehr ähnlich sein.

Format und andere Details 

<ul>
<li>das Format für die Lösung ist (da gibt es ein Checker-Werzeug in der Umgebung geben, was nur dieses Format richtig erkennt, und eure Lösungen entsprechend bewertet):</li>
<ul>
<li>
kein Cycle: 
"s UNSATISFABLE" 
auf stdout, exitcode 20 
</li>
<li>
ein Cycle mit dem Pfad 5->3->4->1->2->5 
"s SATISFIABLE" 
"v 5 3 4 1 2" 
auf stdout, exitcode 10 
</li>
</ul>
<li>
Die Graphen sind eigentlich gerichtet, der Generator liefert für
kleine Graphen meist ungerichtete Graphen, da beide Kanten da sind.
Für größere Graphen ist das nicht garantiert.
</li>
<li>
Der Generator ordnet die Kanten, darauf kann man sich aber nicht
verlassen, falls ich Graphen von außen mit zulasse.
</li>
<li>
Der SAT Solver darf mehrfach aufgerufen werden. Dann interessiert uns was ihr damit genau tut.
</li>
</ul>

Registrierung 
Um an dem Wettbewerb teilnehmen zu können, müssen sich die Team von maximal drei Studenten mit einem Teamnamen, sowie der Namen der Studenten und der Matrikelnummer per Email bis zwei Wochen vor dem Wettbewerb bei Norbert Manthey (Vorname.Nachname at tu-dresden.de) registrieren. Eine Vorabversion des Tools muss bis eine Woche vor dem Wettbewerb eingereicht werden, damit sie auf ihre Lauffähigkeit getestet werden kann (der Wettbewerb wird auf einem Linux System ausgetragen). Der Wettbewerb findet nur statt, wenn sich mindestens drei Teams angemeldet haben.
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Vorstellung der SAT Forschung
|Room=APB E023
|Date=2015/04/13
|DS=DS5
|Download=Satvorstellung-Forschungslinie-SS2015.pdf,Satvorstellung-Forschungslinie-SS2015.pdf,
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Auswertung des Wettbewerbes
|Room=APB E023
|Date=2015/07/06
|DS=DS5
|Download=HamiltonianCycleCompetition-Environment-SS2015.tar.gz,
}}

Datei:HamiltonianCycleCompetition-Environment-SS2015.tar.gz

2015-06-30T08:43:31Z

Norbert Manthey: Norbert Manthey lud eine neue Version von „Datei:HamiltonianCycleCompetition-Environment-SS2015.tar.gz“ hoch

Umgebung für HPC Wettbewerb der Forschungslinie Vorlesung, beinhaltet Graph-Generator

Forschungslinie (SS2015)

2015-06-26T10:56:45Z

Norbert Manthey:

{{Vorlesung
|Title=Forschungslinie
|Research group=Wissensverarbeitung
|Lecturers=Steffen Hölldobler;
|Term=SS
|Year=2015
|SWSLecture=0
|SWSExercise=0
|SWSPractical=0
|Exam type=Hausarbeit
|Description=Diese Vorlesung im Rahmen der Forschungslinien-Vorlesung stellt kurz die Forschung um das Erfüllbarkeitsproblem dar. Weitere Details, auch zu dem damit verbundenen Wettbewerb finden Sie zeitnah auf dieser Webseite.

Wettbewerb 
Es soll ein Löser entwickelt werden, der einen Graphen im DIMACS-Graph-Format einlesen kann, und für diesen Graph einen Hamiltonian-Cycle ausgibt, oder ausgibt, dass es keine Lösung gibt. Im Wettbewerb werden mehrere Graphen gelöst. Der Löser, welcher die meisten Graphen in einem gegebenen Timeout (ca. 10 Minuten) erfolgreich lösen kann, gewinnt. Löser, die eine falsche Lösung ausgeben, werden disqualifiziert. Beispielgraphen gibt es hier: http://mat.gsia.cmu.edu/COLOR/instances.html

Abgabetermin 
Die finale Version des Werkzeugs muss am Freitag, 3.7., bis 24:00 eingereicht worden sein.

Wettbewerbsumgebung 
Unter dem Reiter Termine und Unterlagen wurden Datein für die Wettbewerbungsumgebung und ein Generator für Graphen hinterlegt. Die genutzte Umgebung für den Wettbewerb wird dazu sehr ähnlich sein.

Format und andere Details 

<ul>
<li>das Format für die Lösung ist (da gibt es ein Checker-Werzeug in der Umgebung geben, was nur dieses Format richtig erkennt, und eure Lösungen entsprechend bewertet):</li>
<ul>
<li>
kein Cycle: 
"s UNSATISFABLE" 
auf stdout, exitcode 20 
</li>
<li>
ein Cycle mit dem Pfad 5->3->4->1->2->5 
"s SATISFIABLE" 
"v 5 3 4 1 2" 
auf stdout, exitcode 10 
</li>
</ul>
<li>
Die Graphen sind eigentlich gerichtet, der Generator liefert für
kleine Graphen meist ungerichtete Graphen, da beide Kanten da sind.
Für größere Graphen ist das nicht garantiert.
</li>
<li>
Der Generator ordnet die Kanten, darauf kann man sich aber nicht
verlassen, falls ich Graphen von außen mit zulasse.
</li>
<li>
Der SAT Solver darf mehrfach aufgerufen werden. Dann interessiert uns was ihr damit genau tut.
</li>
</ul>

Registrierung 
Um an dem Wettbewerb teilnehmen zu können, müssen sich die Team von maximal drei Studenten mit einem Teamnamen, sowie der Namen der Studenten und der Matrikelnummer per Email bis zwei Wochen vor dem Wettbewerb bei Norbert Manthey (Vorname.Nachname at tu-dresden.de) registrieren. Eine Vorabversion des Tools muss bis eine Woche vor dem Wettbewerb eingereicht werden, damit sie auf ihre Lauffähigkeit getestet werden kann (der Wettbewerb wird auf einem Linux System ausgetragen). Der Wettbewerb findet nur statt, wenn sich mindestens drei Teams angemeldet haben.
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Vorstellung der SAT Forschung
|Room=APB E023
|Date=2015/04/13
|DS=DS5
|Download=Satvorstellung-Forschungslinie-SS2015.pdf,Satvorstellung-Forschungslinie-SS2015.pdf,
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Auswertung des Wettbewerbes
|Room=APB E023
|Date=2015/07/06
|DS=DS5
|Download=HamiltonianCycleCompetition-Environment-SS2015.tar.gz,HamiltonianCycleCompetition-Environment-SS2015.tar.gz,
}}

Datei:HamiltonianCycleCompetition-Environment-SS2015.tar.gz

2015-06-26T10:56:39Z

Norbert Manthey: Norbert Manthey lud eine neue Version von „Datei:HamiltonianCycleCompetition-Environment-SS2015.tar.gz“ hoch

Umgebung für HPC Wettbewerb der Forschungslinie Vorlesung, beinhaltet Graph-Generator

Forschungslinie (SS2015)

2015-06-26T09:32:54Z

Norbert Manthey:

{{Vorlesung
|Title=Forschungslinie
|Research group=Wissensverarbeitung
|Lecturers=Steffen Hölldobler;
|Term=SS
|Year=2015
|SWSLecture=0
|SWSExercise=0
|SWSPractical=0
|Exam type=Hausarbeit
|Description=Diese Vorlesung im Rahmen der Forschungslinien-Vorlesung stellt kurz die Forschung um das Erfüllbarkeitsproblem dar. Weitere Details, auch zu dem damit verbundenen Wettbewerb finden Sie zeitnah auf dieser Webseite.

Wettbewerb 
Es soll ein Löser entwickelt werden, der einen Graphen im DIMACS-Graph-Format einlesen kann, und für diesen Graph einen Hamiltonian-Cycle ausgibt, oder ausgibt, dass es keine Lösung gibt. Im Wettbewerb werden mehrere Graphen gelöst. Der Löser, welcher die meisten Graphen in einem gegebenen Timeout (ca. 10 Minuten) erfolgreich lösen kann, gewinnt. Löser, die eine falsche Lösung ausgeben, werden disqualifiziert. Beispielgraphen gibt es hier: http://mat.gsia.cmu.edu/COLOR/instances.html

Abgabetermin 
Die finale Version des Werkzeugs muss am Freitag, 3.7., bis 24:00 eingereicht worden sein.

Wettbewerbsumgebung 
Unter dem Reiter Termine und Unterlagen wurden Datein für die Wettbewerbungsumgebung und ein Generator für Graphen hinterlegt. Die genutzte Umgebung für den Wettbewerb wird dazu sehr ähnlich sein.

Format und andere Details 

<ul>
<li>das Format für die Lösung ist (da gibt es ein Checker-Werzeug in der Umgebung geben, was nur dieses Format richtig erkennt, und eure Lösungen entsprechend bewertet):</li>
<ul>
<li>
kein Cycle: 
"s UNSATISFABLE" 
auf stdout, exitcode 20 
</li>
<li>
ein Cycle mit dem Pfad 5->3->4->1->2->5 
"s SATISFIABLE" 
"v 5 3 4 1 2" 
auf stdout, exitcode 10 
</li>
</ul>
<li>
Die Graphen sind eigentlich gerichtet, der Generator liefert für
kleine Graphen meist ungerichtete Graphen, da beide Kanten da sind.
Für größere Graphen ist das nicht garantiert.
</li>
<li>
Der Generator ordnet die Kanten, darauf kann man sich aber nicht
verlassen, falls ich Graphen von außen mit zulasse.
</li>
<li>
Der SAT Solver darf mehrfach aufgerufen werden. Dann interessiert uns was ihr damit genau tut.
</li>
</ul>

Registrierung 
Um an dem Wettbewerb teilnehmen zu können, müssen sich die Team von maximal drei Studenten mit einem Teamnamen, sowie der Namen der Studenten und der Matrikelnummer per Email bis zwei Wochen vor dem Wettbewerb bei Norbert Manthey (Vorname.Nachname at tu-dresden.de) registrieren. Eine Vorabversion des Tools muss bis eine Woche vor dem Wettbewerb eingereicht werden, damit sie auf ihre Lauffähigkeit getestet werden kann (der Wettbewerb wird auf einem Linux System ausgetragen). Der Wettbewerb findet nur statt, wenn sich mindestens drei Teams angemeldet haben.
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Vorstellung der SAT Forschung
|Room=APB E023
|Date=2015/04/13
|DS=DS5
|Download=Satvorstellung-Forschungslinie-SS2015.pdf,Satvorstellung-Forschungslinie-SS2015.pdf,
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Auswertung des Wettbewerbes
|Room=APB E023
|Date=2015/07/06
|DS=DS5
|Download=HamiltonianCycleCompetition-Environment-SS2015.tar.gz,
}}

Forschungslinie (SS2015)

2015-06-26T09:06:45Z

Norbert Manthey:

{{Vorlesung
|Title=Forschungslinie
|Research group=Wissensverarbeitung
|Lecturers=Steffen Hölldobler;
|Term=SS
|Year=2015
|SWSLecture=0
|SWSExercise=0
|SWSPractical=0
|Exam type=Hausarbeit
|Description=Diese Vorlesung im Rahmen der Forschungslinien-Vorlesung stellt kurz die Forschung um das Erfüllbarkeitsproblem dar. Weitere Details, auch zu dem damit verbundenen Wettbewerb finden Sie zeitnah auf dieser Webseite.

Wettbewerb 
Es soll ein Löser entwickelt werden, der einen Graphen im DIMACS-Graph-Format einlesen kann, und für diesen Graph einen Hamiltonian-Cycle ausgibt, oder ausgibt, dass es keine Lösung gibt. Im Wettbewerb werden mehrere Graphen gelöst. Der Löser, welcher die meisten Graphen in einem gegebenen Timeout (ca. 10 Minuten) erfolgreich lösen kann, gewinnt. Löser, die eine falsche Lösung ausgeben, werden disqualifiziert. Beispielgraphen gibt es hier: http://mat.gsia.cmu.edu/COLOR/instances.html

Wettbewerbsumgebung 
Unter dem Reiter Termine und Unterlagen wurden Datein für die Wettbewerbungsumgebung und ein Generator für Graphen hinterlegt. Die genutzte Umgebung für den Wettbewerb wird dazu sehr ähnlich sein.

Format und andere Details 

<ul>
<li>das Format für die Lösung ist (da gibt es ein Checker-Werzeug in der Umgebung geben, was nur dieses Format richtig erkennt, und eure Lösungen entsprechend bewertet):</li>
<ul>
<li>
kein Cycle: 
"s UNSATISFABLE" 
auf stdout, exitcode 20 
</li>
<li>
ein Cycle mit dem Pfad 5->3->4->1->2->5 
"s SATISFIABLE" 
"v 5 3 4 1 2" 
auf stdout, exitcode 10 
</li>
</ul>
<li>
Die Graphen sind eigentlich gerichtet, der Generator liefert für
kleine Graphen meist ungerichtete Graphen, da beide Kanten da sind.
Für größere Graphen ist das nicht garantiert.
</li>
<li>
Der Generator ordnet die Kanten, darauf kann man sich aber nicht
verlassen, falls ich Graphen von außen mit zulasse.
</li>
<li>
Der SAT Solver darf mehrfach aufgerufen werden. Dann interessiert uns was ihr damit genau tut.
</li>
</ul>

Registrierung 
Um an dem Wettbewerb teilnehmen zu können, müssen sich die Team von maximal drei Studenten mit einem Teamnamen, sowie der Namen der Studenten und der Matrikelnummer per Email bis zwei Wochen vor dem Wettbewerb bei Norbert Manthey (Vorname.Nachname at tu-dresden.de) registrieren. Eine Vorabversion des Tools muss bis eine Woche vor dem Wettbewerb eingereicht werden, damit sie auf ihre Lauffähigkeit getestet werden kann (der Wettbewerb wird auf einem Linux System ausgetragen). Der Wettbewerb findet nur statt, wenn sich mindestens drei Teams angemeldet haben.
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Vorstellung der SAT Forschung
|Room=APB E023
|Date=2015/04/13
|DS=DS5
|Download=Satvorstellung-Forschungslinie-SS2015.pdf,Satvorstellung-Forschungslinie-SS2015.pdf,
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Auswertung des Wettbewerbes
|Room=APB E023
|Date=2015/07/06
|DS=DS5
|Download=HamiltonianCycleCompetition-Environment-SS2015.tar.gz,
}}

SAT-Solving und das Lösen von Sudokus (SS2015)

2015-06-16T13:05:52Z

Norbert Manthey:

Datei:SAT-Solving-Algorithms2015.pdf

2015-06-16T13:05:45Z

Norbert Manthey: slides to describe sat algorithms

slides to describe sat algorithms

SummerSchool2015/en

2015-06-15T17:55:45Z

Norbert Manthey:

{{DISPLAYTITLE:ICCL Summer School 'Reasoning', September 13 - 26, 2015, Dresden }}

In September 2015 we organize a summer school, which, in the second week, will be held at the same time as the [http://www.tu-dresden.de/inf/ki2015 German AI conference].
The conference and the summer school will be coupled.
A participation in the summer school includes the free participation in the AI conference.

We encourage participants of the summer school to submit own research work to the [http://ki2015.computational-logic.org/submission.php German AI conference] or to one of their [http://ki2015.computational-logic.org/workshops.php workshops].

As in the past summer schools at TU Dresden in
[http://www.computational-logic.org/iccl/events/WPT-2002 2002],
[http://www.computational-logic.org/iccl/events/WPT-2003 2003],
[http://www.computational-logic.org/iccl/events/SA-2004 2004],
[http://www.computational-logic.org/content/events/iccl-ss-2005 2005],
[http://www.computational-logic.org/content/events/iccl-ss-2006 2006],
[http://reasoningweb.org/2007/ 2007],
[http://www.computational-logic.org/content/events/iccl-ss-2008 2008]
[http://www.computational-logic.org/content/events/iccl-ss-2010 2010] and
[http://www.computational-logic.org/content/events/iccl-ss-2013 2013]
people from distinct, but communicating communities will gather in an informal and friendly atmosphere.
This two-week event is aimed at graduate students, researchers and practitioners.

''' Topic '''

The topic of this year's summer school is '''Reasoning'''

{{#maketabs:|Info and Venue=

''' Dates '''

* Arrival: 13th of September
* Registration: 14th of September
* Departure: 26th of September

''' Venue '''

The summer school is held at the Computer Science Faculty building of Technische Universität Dresden, Nöthnitzer Straße 46, Dresden-Räcknitz .

''' How to reach us '''

* Directions [http://www.inf.tu-dresden.de/index.php?node_id=12&ln=en]
* Annotated satellite map [http://maps.google.com/maps?f=q&hl=en&geocode=&q=N%C3%B6thnitzer+Stra%C3%9Fe+46,+Dresden&jsv=107&sll=37.0625,-95.677068&sspn=49.490703,82.265625&ie=UTF8&ll=51.026389,13.720336&spn=0.009677,0.020084&t=h&z=16&iwloc=addr]

''' Public Transport '''

Dresden provides many nice places to be, such that you might want to use public transport.

For the participants, we can provide tickets for public transport during the summer school (it is valid for the two weeks, from 13. to 26.September)
for 29 EUR.

Tickets without discount have the following price: Single Ticket: 2,20 EUR, Four Tickets: 8 EUR, Day Ticket: 6 EUR, Week Ticket: 21 EUR

[[File:Faculty-Computerscience.jpg|upright|center|alt=Faculty of computer science.|Faculty of computer science.]]

''' Weather Information '''

In this period of the year, the average temperature at daytime in Dresden will be about 24 degrees. It may be windy; sometimes it rains. However, if there is a longer raining period, the maximum temperature might decrease to about 15 degrees. This year the weather is rather hot. To be on the save side, please check [http://www.weather24.com].

''' Computing Facilities '''

* We provide access to wireless networking in the ground floor of the Computer Science Faculty building during the Summer School. If you don't have a notebook with wireless networking, we can provide you a login account for the department computing center.

* You will receive your personal login name and password as well as a short explanation during the registration.

* Please note, that certain internet services (e. g. SMTP) might not be available due to the security policies of our university. To access these services, we suggest you the usage of a VPN service of your university.

* Please note we will not provide any facilities or services for personal printing.

|Lecturers and Lectures=

''' Term Rewriting Systems (5h) '''
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 (3h) '''
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]], [http://portal.uni-freiburg.de/cognition/mitarbeiter/ragni/ 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 (4h) '''
by [http://www.cs.uni-potsdam.de/~torsten/ 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.

|Registration=

The summer school '''Reasoning''' is a platform for knowledge transfer within a very rapid increasing research community in the field of '''Computational Logic'''. We will offer introductory courses covering the fundamentals of reasoning, courses at advanced levels, as well as applied courses dedicated to specialized topics and the state of the art. All lecturers are leading researchers in their field and have been awarded prizes. For the participants of the summer school, the participation at the 38th German AI conference, also held in Dresden, is free of charge.

''' Registration '''

If you want to register for the ICCL Summer School 2015, please be informed about our social program and the summer school ticket beforehand, as questions about it will be asked in the registration. Then, please fill the [http://www.computational-logic.org/content/events/iccl-ss-2015/register/general.php online-registration form].

''' Admission Requirements '''

The summer school is for master and phd students who work in a discipline which is relevant for the summer school. However, excellent bachelor students are also approved.

''' Fees '''

We ask for a participation fee

* Early Bird Registration (Deadline 11.05.2015)
** Students: 200 EUR
** Academic 300 EUR
** Others 500 EUR

* Late Registration
** Students: 300 EUR
** Academic 450 EUR
** Others 900 EUR

Please pay this summer school fee cash at the day of your arrival.
On request, you may also make a bank transfer. Any fees arising for the transfer must be paid by you and cannot be deducted from the registration fee.

If belonging to the university sector, you have to provide some respective evidence when paying the fees at the check-in (e. g. student card, web page at a university etc.).
Students must present a proof of their status (student id in case of a bachelor, master or diplom student; scholarship certificate in case of PhD students) upon arrival at the summer shool or conference.

''' Grants '''

A limited number of grants for students and university employees will be available, which includes a waiver of the participation fee.

Please indicate in your application, if the only possibility for you to participate is via a grant. Applications for grants must include an estimate of travel costs (to be mentioned in the respective part of the online registration form).

The deadline for the application for this grant is the same as for the early bird registration, 11.05.2015.

|Timetable=

Note, we might provide the opportunity to allow participants of the summer school to give short presentations about their current work.
If you are willing to give such a presentation, please give the according information in the registration form.

The registration is on Monday, 14.9. and Tuesday, 15.9.2015, between 8 and 14 o'clock at Susan Gierth's office in APB2002. In case you can't come during these times, you can contact her by email: susann.gierth@tu-dresden.de

<h4>First Week</h4>

<table style="text-align: center" border="1">
<tr>
<th> </th>
<th> Sunday 
  September 13 </th>
<th> Monday 
  September 14 </th>
<th> Tuesday 
  September 15 </th>
<th> Wednesday 
  September 16 </th>
<th> Thursday 
  September 17 </th>
<th> Friday 
  September 18 </th>
<th> Saturday 
  September 19 </th>
</tr>
<tr>
<th>   9:00 - 10:00</th>
<td> </td>
<td>Opening</td>
<td>Baier</td>
<td>Gaggl</td>
<td>Gaggl</td>
<td>Baader</td>
<td>Excursion</td>
</tr>
<tr>
<th>10:20 - 11:20</th>
<td> </td>
<td>HM</td>
<td>Baier</td>
<td>DHR</td>
<td>DHR</td>
<td>Baader</td>
<td>Excursion</td>
</tr>
<tr>
<th>11:40 - 12:40</th>
<td> </td>
<td>DHR</td>
<td>Baier</td>
<td>Excursion</td>
<td>DHR</td>
<td>Baader</td>
<td>Excursion</td>
</tr>
<tr>
<th>14:40 - 15:40</th>
<td> </td>
<td>Gaggl</td>
<td>Gaggl</td>
<td>Excursion</td>
<td>Baader</td>
<td>free</td>
<td>Excursion</td>
</tr>
<tr>
<th>16:00 - 17:00</th>
<td> </td>
<td>Gaggl</td>
<td>DHR</td>
<td>Excursion</td>
<td>Baader</td>
<td>free</td>
<td>Excursion</td>
</tr>
<tr>
<th>Evening</th>
<td> </td>
<td> </td>
<td> </td>
<td>Excursion</td>
<td> </td>
<td> </td>
<td>Excursion</td>
</tr>
</table>
 

<h4>Second Week</h4>

<table style="text-align: center" border="1">
<tr>
<th> </th>
<th> Sunday 
  September 20 </th>
<th> Monday 
  September 21 </th>
<th> Tuesday 
  September 22 </th>
<th> Wednesday 
  September 23 </th>
<th> Thursday 
  September 24 </th>
<th> Friday 
  September 25 </th>
<th> Saturday 
  September 26 </th>
</tr>
<tr>
<th>   9:00 - 10:00</th>
<td> </td>
<td>HM</td>
<td>Rudolph</td>
<td>KI 2015</td>
<td>Schaub</td>
<td>Schaub</td>
<td> </td>
</tr>
<tr>
<th>10:20 - 11:20</th>
<td> </td>
<td>HM</td>
<td>Rudolph</td>
<td>KI 2015</td>
<td>Schaub</td>
<td>Schaub</td>
<td> </td>
</tr>
<tr>
<th>11:40 - 12.40</th>
<td> </td>
<td>Krötzsch</td>
<td>HM</td>
<td>KI 2015</td>
<td>KI 2015</td>
<td>KI 2015</td>
<td> </td>
</tr>
<tr>
<th>14.40 - 15.40</th>
<td> </td>
<td>Krötzsch</td>
<td>HM</td>
<td>KI 2015</td>
<td>KI 2015</td>
<td>KI 2015</td>
<td> </td>
</tr>
<tr>
<th>16.00 - 17.00</th>
<td> </td>
<td>Krötzsch</td>
<td>free</td>
<td>KI 2015</td>
<td>KI 2015</td>
<td>KI 2015</td>
<td> </td>
</tr>
<tr>
<th>Evening</th>
<td> </td>
<td> </td>
<td>Reception</td>
<td> </td>
<td>Dinner</td>
<td> </td>
<td> </td>
</tr>
</table>

HM = Hölldobler, Manthey
DHR = Dietz, Hölldobler, Ragni

|Social Program=
We plan to do the following social activities during the summer school. Yet, the details are not fixed.

* Walking City Tour (Tuesday, 15.9.)
* Excursion to Pirna (Wednesday, 16.9.)
* Excursion to Saxon Switzerland (Saturday, 19.9.)
* Reception (together with KI 2015, Tuesday, 22.9.)
* Dinner at Eckberg Castle (Thursday, 24.9. for grant holders, academic and others; students will given free tickets if available)

The Dinner at Eckberg Castle has the following menu:
* Thin slices of veal saddle marinated with boletus Melon chutney, raspberry dressing
** (vegetarian: Fresh salad with boletus, Melon chutney, raspberry dressing )
* Fried chicken breast sweet potato puree, young spinach melted tomatoes
** (vegetarian: Mixed vegetables with sweet potato puree, young spinach, melted tomatoes )
* Marinated pineapple chocolate tartlet and sorbet

|Stay in Dresden=

'''Accomodation'''

Some hotels and apartment agencies offer accommodation to participants.

All suggested places are conveniently connected by public transportation to the summer school and workshop venue.

Please act fast, because it´s very difficult to find rooms in Dresden in this period of the year. Here, we provide a list of [https://ddll.inf.tu-dresden.de/web/Accomodation/en well located and affordable accommodation].

'''Living Expenses'''

* Accommodation: The costs for accommodation depend on the place, where you book a room and can be found on the web pages linked from the page above.
* Living: For food and living no exact information can be given as this is too individual. A calculation for Saxon law amounts to 24 EUR per day.
* Public transportation: If you want to use public transports, please see [[Info and Venue]] for the ticket fares and possibilities.
* Cultural program: We don't charge any addition for our cultural program. Only for some single events you may need some little money for food etc. as mentioned on the event information pages.
* Per diems: The per diems rates for Germany given by the European Commission amount to 208 EUR. These rates include all arising costs as mentioned above.

'''Child Care'''

A flexible child care is offered to participants of congresses or other events taking place at the Technische Universität Dresden.
It gives you the possibility to take your children to Dresden and leave them under care of educated staff, when attending lectures.

For more information, please contact:

Campusbüro Uni mit Kind

George-Bähr-Straße 1b

Tel./Fax: +49-351-463-32666 / -32667

E-mail: campusbuero@tu-dresden.de

[http://kinder.studentenwerk-dresden.de/ German web page]

|Chairs and Organizers=

'''Chair of the Summer School''' [[ Steffen Hölldobler]]

'''Organizers of the Summer School''' [[Emmanuelle Dietz]], [[Julia Koppenhagen]], [[Norbert Manthey]]

}}

PSAT

2015-06-11T07:57:31Z

Norbert Manthey:

{{Projekt
|Kurzname=PSAT
|Name=Paralleles Lösen des Erfüllbarkeitproblems
|Name EN=Parallel Satisfiability Testing
|Beschreibung DE=Das Erfüllbarkeitsproblem (SAT) ist ein Standartproblem der Komplexitätsklasse NP mit einer sehr einfachen, aber generischen, Eingabesprache. Durch die Entwicklung der SAT Systeme in den letzten 20 Jahren wird SAT heute genutzt, um Chip-Designs zu verifizieren, um Planungsprobleme wie Car-Sqeuencing zu lösen, um Eigenschaften von Konfigurationen zu verifizieren, oder um Fahrpläne für Bahnnetzwerke zu generieren. Viele weitere diskrete Entscheidungsprobleme können mit Hilfe von SAT gelöst werden. Außerdem können diskrete Optimierungsprobleme auf SAT abgebildet werden und durch mehrfaches Aufrufen des SAT Systems gelöst werden.

In diesem Projekt sollen parallele SAT Systeme entstehen, welche es erlauben auf modernen Mehrkernsystemen, sowie auf Hochleistungsrechnern das Erfüllbarkeitsproblem schneller zu lösen, als es mit sequentiellen Methoden derzeit möglich ist.
|Beschreibung EN=Satisfiability testing is one of the representative problems of the complexity class NP with a simple, but very generic, input language. Due to the significant improvements of the 20 years SAT is used nowadays to verify chip designs, to solve planning problems such as car sequencing, to prove properties of configuration specifications, or to generate schedules for train networks. Many more discrete decision problems can be solved with SAT technology. Furthermore, discrete optimization problems can also be solved by calling a SAT solver multiple times.

In the project a parallel SAT solver should be developed, which can exploit the modern multi-core architecture as well as high performance clusters to solve satisfiability testing more efficient than with the current sequential algorithms.
|Kontaktperson=Norbert Manthey,
|Project Authors=Norbert Manthey, Steffen Hölldobler,
|Start=2015/01/01
|Finanziert von=DFG
|Projektstatus=aktiv
|Person=Norbert Manthey, Steffen Hölldobler,
|Forschungsgruppe=Wissensverarbeitung
}}

SummerSchool2015/en

2015-06-11T07:55:58Z

Norbert Manthey:

{{DISPLAYTITLE:ICCL Summer School 'Reasoning', September 13 - 26, 2015, Dresden }}

In September 2015 we organize a summer school, which, in the second week, will be held at the same time as the [http://www.tu-dresden.de/inf/ki2015 German AI conference].
The conference and the summer school will be coupled.
A participation in the summer school includes the free participation in the AI conference.

We encourage participants of the summer school to submit own research work to the [http://ki2015.computational-logic.org/submission.php German AI conference] or to one of their [http://ki2015.computational-logic.org/workshops.php workshops].

As in the past summer schools at TU Dresden in
[http://www.computational-logic.org/iccl/events/WPT-2002 2002],
[http://www.computational-logic.org/iccl/events/WPT-2003 2003],
[http://www.computational-logic.org/iccl/events/SA-2004 2004],
[http://www.computational-logic.org/content/events/iccl-ss-2005 2005],
[http://www.computational-logic.org/content/events/iccl-ss-2006 2006],
[http://reasoningweb.org/2007/ 2007],
[http://www.computational-logic.org/content/events/iccl-ss-2008 2008]
[http://www.computational-logic.org/content/events/iccl-ss-2010 2010] and
[http://www.computational-logic.org/content/events/iccl-ss-2013 2013]
people from distinct, but communicating communities will gather in an informal and friendly atmosphere.
This two-week event is aimed at graduate students, researchers and practitioners.

''' Topic '''

The topic of this year's summer school is '''Reasoning'''

{{#maketabs:|Info and Venue=

''' Dates '''

* Arrival: 13th of September
* Registration: 14th of September
* Departure: 26th of September

''' Venue '''

The summer school is held at the Computer Science Faculty building of Technische Universität Dresden, Nöthnitzer Straße 46, Dresden-Räcknitz .

''' How to reach us '''

* Directions [http://www.inf.tu-dresden.de/index.php?node_id=12&ln=en]
* Annotated satellite map [http://maps.google.com/maps?f=q&hl=en&geocode=&q=N%C3%B6thnitzer+Stra%C3%9Fe+46,+Dresden&jsv=107&sll=37.0625,-95.677068&sspn=49.490703,82.265625&ie=UTF8&ll=51.026389,13.720336&spn=0.009677,0.020084&t=h&z=16&iwloc=addr]

''' Public Transport '''

Dresden provides many nice places to be, such that you might want to use public transport.

For the participants, we can provide tickets for public transport during the summer school (it is valid for the two weeks, from 13. to 26.September)
for 29 EUR.

Tickets without discount have the following price: Single Ticket: 2,20 EUR, Four Tickets: 8 EUR, Day Ticket: 6 EUR, Week Ticket: 21 EUR

[[File:Faculty-Computerscience.jpg|upright|center|alt=Faculty of computer science.|Faculty of computer science.]]

''' Weather Information '''

In this period of the year, the average temperature at daytime in Dresden will be about 24 degrees. It may be windy; sometimes it rains. However, if there is a longer raining period, the maximum temperature might decrease to about 15 degrees. This year the weather is rather hot. To be on the save side, please check [http://www.weather24.com].

''' Computing Facilities '''

* We provide access to wireless networking in the ground floor of the Computer Science Faculty building during the Summer School. If you don't have a notebook with wireless networking, we can provide you a login account for the department computing center.

* You will receive your personal login name and password as well as a short explanation during the registration.

* Please note, that certain internet services (e. g. SMTP) might not be available due to the security policies of our university. To access these services, we suggest you the usage of a VPN service of your university.

* Please note we will not provide any facilities or services for personal printing.

|Lecturers and Lectures=

''' Term Rewriting Systems (5h) '''
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 (3h) '''
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]], [http://portal.uni-freiburg.de/cognition/mitarbeiter/ragni/ 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 (4h) '''
by [http://www.cs.uni-potsdam.de/~torsten/ 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.

|Registration=

The summer school '''Reasoning''' is a platform for knowledge transfer within a very rapid increasing research community in the field of '''Computational Logic'''. We will offer introductory courses covering the fundamentals of reasoning, courses at advanced levels, as well as applied courses dedicated to specialized topics and the state of the art. All lecturers are leading researchers in their field and have been awarded prizes. For the participants of the summer school, the participation at the 38th German AI conference, also held in Dresden, is free of charge.

''' Registration '''

If you want to register for the ICCL Summer School 2015, please be informed about our social program and the summer school ticket beforehand, as questions about it will be asked in the registration. Then, please fill the [http://www.computational-logic.org/content/events/iccl-ss-2015/register/general.php online-registration form].

''' Admission Requirements '''

The summer school is for master and phd students who work in a discipline which is relevant for the summer school. However, excellent bachelor students are also approved.

''' Fees '''

We ask for a participation fee

* Early Bird Registration (Deadline 11.05.2015)
** Students: 200 EUR
** Academic 300 EUR
** Others 500 EUR

* Late Registration
** Students: 300 EUR
** Academic 450 EUR
** Others 900 EUR

Please pay this summer school fee cash at the day of your arrival.
On request, you may also make a bank transfer. Any fees arising for the transfer must be paid by you and cannot be deducted from the registration fee.

If belonging to the university sector, you have to provide some respective evidence when paying the fees at the check-in (e. g. student card, web page at a university etc.).

''' Grants '''

A limited number of grants for students and university employees will be available, which includes a waiver of the participation fee.

Please indicate in your application, if the only possibility for you to participate is via a grant. Applications for grants must include an estimate of travel costs (to be mentioned in the respective part of the online registration form).

The deadline for the application for this grant is the same as for the early bird registration, 11.05.2015.

|Timetable=

Note, we might provide the opportunity to allow participants of the summer school to give short presentations about their current work.
If you are willing to give such a presentation, please give the according information in the registration form.

The registration is on Monday, 14.9. and Tuesday, 15.9.2015, between 8 and 14 o'clock at Susan Gierth's office in APB2002. In case you can't come during these times, you can contact her by email: susann.gierth@tu-dresden.de

<h4>First Week</h4>

<table style="text-align: center" border="1">
<tr>
<th> </th>
<th> Sunday 
  September 13 </th>
<th> Monday 
  September 14 </th>
<th> Tuesday 
  September 15 </th>
<th> Wednesday 
  September 16 </th>
<th> Thursday 
  September 17 </th>
<th> Friday 
  September 18 </th>
<th> Saturday 
  September 19 </th>
</tr>
<tr>
<th>   9:00 - 10:00</th>
<td> </td>
<td>Opening</td>
<td>Baier</td>
<td>Gaggl</td>
<td>Gaggl</td>
<td>Baader</td>
<td>Excursion</td>
</tr>
<tr>
<th>10:20 - 11:20</th>
<td> </td>
<td>HM</td>
<td>Baier</td>
<td>DHR</td>
<td>DHR</td>
<td>Baader</td>
<td>Excursion</td>
</tr>
<tr>
<th>11:40 - 12:40</th>
<td> </td>
<td>DHR</td>
<td>Baier</td>
<td>Excursion</td>
<td>DHR</td>
<td>Baader</td>
<td>Excursion</td>
</tr>
<tr>
<th>14:40 - 15:40</th>
<td> </td>
<td>Gaggl</td>
<td>Gaggl</td>
<td>Excursion</td>
<td>Baader</td>
<td>free</td>
<td>Excursion</td>
</tr>
<tr>
<th>16:00 - 17:00</th>
<td> </td>
<td>Gaggl</td>
<td>DHR</td>
<td>Excursion</td>
<td>Baader</td>
<td>free</td>
<td>Excursion</td>
</tr>
<tr>
<th>Evening</th>
<td> </td>
<td> </td>
<td> </td>
<td>Excursion</td>
<td> </td>
<td> </td>
<td>Excursion</td>
</tr>
</table>
 

<h4>Second Week</h4>

<table style="text-align: center" border="1">
<tr>
<th> </th>
<th> Sunday 
  September 20 </th>
<th> Monday 
  September 21 </th>
<th> Tuesday 
  September 22 </th>
<th> Wednesday 
  September 23 </th>
<th> Thursday 
  September 24 </th>
<th> Friday 
  September 25 </th>
<th> Saturday 
  September 26 </th>
</tr>
<tr>
<th>   9:00 - 10:00</th>
<td> </td>
<td>HM</td>
<td>Rudolph</td>
<td>KI 2015</td>
<td>Schaub</td>
<td>Schaub</td>
<td> </td>
</tr>
<tr>
<th>10:20 - 11:20</th>
<td> </td>
<td>HM</td>
<td>Rudolph</td>
<td>KI 2015</td>
<td>Schaub</td>
<td>Schaub</td>
<td> </td>
</tr>
<tr>
<th>11:40 - 12.40</th>
<td> </td>
<td>Krötzsch</td>
<td>HM</td>
<td>KI 2015</td>
<td>KI 2015</td>
<td>KI 2015</td>
<td> </td>
</tr>
<tr>
<th>14.40 - 15.40</th>
<td> </td>
<td>Krötzsch</td>
<td>HM</td>
<td>KI 2015</td>
<td>KI 2015</td>
<td>KI 2015</td>
<td> </td>
</tr>
<tr>
<th>16.00 - 17.00</th>
<td> </td>
<td>Krötzsch</td>
<td>free</td>
<td>KI 2015</td>
<td>KI 2015</td>
<td>KI 2015</td>
<td> </td>
</tr>
<tr>
<th>Evening</th>
<td> </td>
<td> </td>
<td>Reception</td>
<td> </td>
<td>Dinner</td>
<td> </td>
<td> </td>
</tr>
</table>

HM = Hölldobler, Manthey
DHR = Dietz, Hölldobler, Ragni

|Social Program=
We plan to do the following social activities during the summer school. Yet, the details are not fixed.

* Walking City Tour (Tuesday, 15.9.)
* Excursion to Pirna (Wednesday, 16.9.)
* Excursion to Saxon Switzerland (Saturday, 19.9.)
* Reception (together with KI 2015, Tuesday, 22.9.)
* Dinner at Eckberg Castle (Thursday, 24.9. for grant holders, academic and others; students will given free tickets if available)

The Dinner at Eckberg Castle has the following menu:
* Thin slices of veal saddle marinated with boletus Melon chutney, raspberry dressing
** (vegetarian: Fresh salad with boletus, Melon chutney, raspberry dressing )
* Fried chicken breast sweet potato puree, young spinach melted tomatoes
** (vegetarian: Mixed vegetables with sweet potato puree, young spinach, melted tomatoes )
* Marinated pineapple chocolate tartlet and sorbet

|Stay in Dresden=

'''Accomodation'''

Some hotels and apartment agencies offer accommodation to participants.

All suggested places are conveniently connected by public transportation to the summer school and workshop venue.

Please act fast, because it´s very difficult to find rooms in Dresden in this period of the year. Here, we provide a list of [https://ddll.inf.tu-dresden.de/web/Accomodation/en well located and affordable accommodation].

'''Living Expenses'''

* Accommodation: The costs for accommodation depend on the place, where you book a room and can be found on the web pages linked from the page above.
* Living: For food and living no exact information can be given as this is too individual. A calculation for Saxon law amounts to 24 EUR per day.
* Public transportation: If you want to use public transports, please see [[Info and Venue]] for the ticket fares and possibilities.
* Cultural program: We don't charge any addition for our cultural program. Only for some single events you may need some little money for food etc. as mentioned on the event information pages.
* Per diems: The per diems rates for Germany given by the European Commission amount to 208 EUR. These rates include all arising costs as mentioned above.

'''Child Care'''

A flexible child care is offered to participants of congresses or other events taking place at the Technische Universität Dresden.
It gives you the possibility to take your children to Dresden and leave them under care of educated staff, when attending lectures.

For more information, please contact:

Campusbüro Uni mit Kind

George-Bähr-Straße 1b

Tel./Fax: +49-351-463-32666 / -32667

E-mail: campusbuero@tu-dresden.de

[http://kinder.studentenwerk-dresden.de/ German web page]

|Chairs and Organizers=

'''Chair of the Summer School''' [[ Steffen Hölldobler]]

'''Organizers of the Summer School''' [[Emmanuelle Dietz]], [[Julia Koppenhagen]], [[Norbert Manthey]]

}}

Forschungslinie (SS2015)

2015-06-01T08:56:57Z

Norbert Manthey:

Datei:HamiltonianCycleCompetition-Environment-SS2015.tar.gz

2015-06-01T08:55:30Z

Norbert Manthey: Umgebung für HPC Wettbewerb der Forschungslinie Vorlesung, beinhaltet Graph-Generator

Umgebung für HPC Wettbewerb der Forschungslinie Vorlesung, beinhaltet Graph-Generator

SummerSchool2015/en

2015-05-22T11:35:13Z

Norbert Manthey:

{{DISPLAYTITLE:ICCL Summer School 'Reasoning', September 13 - 26, 2015, Dresden }}

In September 2015 we organize a summer school, which, in the second week, will be held at the same time as the [http://www.tu-dresden.de/inf/ki2015 German AI conference].
The conference and the summer school will be coupled.
A participation in the summer school includes the free participation in the AI conference.

We encourage participants of the summer school to submit own research work to the [http://ki2015.computational-logic.org/submission.php German AI conference] or to one of their [http://ki2015.computational-logic.org/workshops.php workshops].

As in the past summer schools at TU Dresden in
[http://www.computational-logic.org/iccl/events/WPT-2002 2002],
[http://www.computational-logic.org/iccl/events/WPT-2003 2003],
[http://www.computational-logic.org/iccl/events/SA-2004 2004],
[http://www.computational-logic.org/content/events/iccl-ss-2005 2005],
[http://www.computational-logic.org/content/events/iccl-ss-2006 2006],
[http://reasoningweb.org/2007/ 2007],
[http://www.computational-logic.org/content/events/iccl-ss-2008 2008]
[http://www.computational-logic.org/content/events/iccl-ss-2010 2010] and
[http://www.computational-logic.org/content/events/iccl-ss-2013 2013]
people from distinct, but communicating communities will gather in an informal and friendly atmosphere.
This two-week event is aimed at graduate students, researchers and practitioners.

''' Topic '''

The topic of this year's summer school is '''Reasoning'''

{{#maketabs:|Info and Venue=

''' Dates '''

* Arrival: 13th of September
* Registration: 14th of September
* Departure: 26th of September

''' Venue '''

The summer school is held at the Computer Science Faculty building of Technische Universität Dresden, Nöthnitzer Straße 46, Dresden-Räcknitz .

''' How to reach us '''

* Directions [http://www.inf.tu-dresden.de/index.php?node_id=12&ln=en]
* Annotated satellite map [http://maps.google.com/maps?f=q&hl=en&geocode=&q=N%C3%B6thnitzer+Stra%C3%9Fe+46,+Dresden&jsv=107&sll=37.0625,-95.677068&sspn=49.490703,82.265625&ie=UTF8&ll=51.026389,13.720336&spn=0.009677,0.020084&t=h&z=16&iwloc=addr]

''' Public Transport '''

Dresden provides many nice places to be, such that you might want to use public transport.

For the participants, we can provide tickets for public transport during the summer school (it is valid for the two weeks, from 13. to 26.September)
for 29 EUR.

Tickets without discount have the following price: Single Ticket: 2,20 EUR, Four Tickets: 8 EUR, Day Ticket: 6 EUR, Week Ticket: 21 EUR

[[File:Faculty-Computerscience.jpg|upright|center|alt=Faculty of computer science.|Faculty of computer science.]]

''' Weather Information '''

In this period of the year, the average temperature at daytime in Dresden will be about 24 degrees. It may be windy; sometimes it rains. However, if there is a longer raining period, the maximum temperature might decrease to about 15 degrees. This year the weather is rather hot. To be on the save side, please check [http://www.weather24.com].

''' Computing Facilities '''

* We provide access to wireless networking in the ground floor of the Computer Science Faculty building during the Summer School. If you don't have a notebook with wireless networking, we can provide you a login account for the department computing center.

* You will receive your personal login name and password as well as a short explanation during the registration.

* Please note, that certain internet services (e. g. SMTP) might not be available due to the security policies of our university. To access these services, we suggest you the usage of a VPN service of your university.

* Please note we will not provide any facilities or services for personal printing.

|Lecturers and Lectures=

''' Term Rewriting Systems (5h) '''
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 (3h) '''
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]], [http://portal.uni-freiburg.de/cognition/mitarbeiter/ragni/ 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 (4h) '''
by [http://www.cs.uni-potsdam.de/~torsten/ 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.

|Registration=

The summer school '''Reasoning''' is a platform for knowledge transfer within a very rapid increasing research community in the field of '''Computational Logic'''. We will offer introductory courses covering the fundamentals of reasoning, courses at advanced levels, as well as applied courses dedicated to specialized topics and the state of the art. All lecturers are leading researchers in their field and have been awarded prizes. For the participants of the summer school, the participation at the 38th German AI conference, also held in Dresden, is free of charge.

''' Registration '''

If you want to register for the ICCL Summer School 2015, please be informed about our social program and the summer school ticket beforehand, as questions about it will be asked in the registration. Then, please fill the [http://www.computational-logic.org/content/events/iccl-ss-2015/register/general.php online-registration form].

''' Admission Requirements '''

The summer school is for master and phd students who work in a discipline which is relevant for the summer school. However, excellent bachelor students are also approved.

''' Fees '''

We ask for a participation fee

* Early Bird Registration (Deadline 11.05.2015)
** Students: 200 EUR
** Academic 300 EUR
** Others 500 EUR

* Late Registration
** Students: 300 EUR
** Academic 450 EUR
** Others 900 EUR

Please pay this summer school fee cash at the day of your arrival.
On request, you may also make a bank transfer. Any fees arising for the transfer must be paid by you and cannot be deducted from the registration fee.

If belonging to the university sector, you have to provide some respective evidence when paying the fees at the check-in (e. g. student card, web page at a university etc.).

''' Grants '''

A limited number of grants for students and university employees will be available, which includes a waiver of the participation fee.

Please indicate in your application, if the only possibility for you to participate is via a grant. Applications for grants must include an estimate of travel costs (to be mentioned in the respective part of the online registration form).

The deadline for the application for this grant is the same as for the early bird registration, 11.05.2015.

|Timetable=

Note, we might provide the opportunity to allow participants of the summer school to give short presentations about their current work.
If you are willing to give such a presentation, please give the according information in the registration form.

The registration is on Monday, 14.9.2015 between 8 and 9 o'clock and in all breaks of the first week.
<h4>First Week</h4>

<table style="text-align: center" border="1">
<tr>
<th> </th>
<th> Sunday 
  September 13 </th>
<th> Monday 
  September 14 </th>
<th> Tuesday 
  September 15 </th>
<th> Wednesday 
  September 16 </th>
<th> Thursday 
  September 17 </th>
<th> Friday 
  September 18 </th>
<th> Saturday 
  September 19 </th>
</tr>
<tr>
<th>   9:00 - 10:00</th>
<td> </td>
<td>Opening</td>
<td>Baier</td>
<td>Gaggl</td>
<td>Gaggl</td>
<td>Baader</td>
<td>Excursion</td>
</tr>
<tr>
<th>10:20 - 11:20</th>
<td> </td>
<td>HM</td>
<td>Baier</td>
<td>DHR</td>
<td>DHR</td>
<td>Baader</td>
<td>Excursion</td>
</tr>
<tr>
<th>11:40 - 12:40</th>
<td> </td>
<td>DHR</td>
<td>Baier</td>
<td>Excursion</td>
<td>DHR</td>
<td>Baader</td>
<td>Excursion</td>
</tr>
<tr>
<th>14:40 - 15:40</th>
<td> </td>
<td>Gaggl</td>
<td>Gaggl</td>
<td>Excursion</td>
<td>Baader</td>
<td>free</td>
<td>Excursion</td>
</tr>
<tr>
<th>16:00 - 17:00</th>
<td> </td>
<td>Gaggl</td>
<td>DHR</td>
<td>Excursion</td>
<td>Baader</td>
<td>free</td>
<td>Excursion</td>
</tr>
<tr>
<th>Evening</th>
<td> </td>
<td> </td>
<td> </td>
<td>Excursion</td>
<td> </td>
<td> </td>
<td>Excursion</td>
</tr>
</table>
 

<h4>Second Week</h4>

<table style="text-align: center" border="1">
<tr>
<th> </th>
<th> Sunday 
  September 20 </th>
<th> Monday 
  September 21 </th>
<th> Tuesday 
  September 22 </th>
<th> Wednesday 
  September 23 </th>
<th> Thursday 
  September 24 </th>
<th> Friday 
  September 25 </th>
<th> Saturday 
  September 26 </th>
</tr>
<tr>
<th>   9:00 - 10:00</th>
<td> </td>
<td>HM</td>
<td>Rudolph</td>
<td>KI 2015</td>
<td>Schaub</td>
<td>Schaub</td>
<td> </td>
</tr>
<tr>
<th>10:20 - 11:20</th>
<td> </td>
<td>HM</td>
<td>Rudolph</td>
<td>KI 2015</td>
<td>Schaub</td>
<td>Schaub</td>
<td> </td>
</tr>
<tr>
<th>11:40 - 12.40</th>
<td> </td>
<td>Krötzsch</td>
<td>HM</td>
<td>KI 2015</td>
<td>KI 2015</td>
<td>KI 2015</td>
<td> </td>
</tr>
<tr>
<th>14.40 - 15.40</th>
<td> </td>
<td>Krötzsch</td>
<td>HM</td>
<td>KI 2015</td>
<td>KI 2015</td>
<td>KI 2015</td>
<td> </td>
</tr>
<tr>
<th>16.00 - 17.00</th>
<td> </td>
<td>Krötzsch</td>
<td>free</td>
<td>KI 2015</td>
<td>KI 2015</td>
<td>KI 2015</td>
<td> </td>
</tr>
<tr>
<th>Evening</th>
<td> </td>
<td> </td>
<td>Reception</td>
<td> </td>
<td>Dinner</td>
<td> </td>
<td> </td>
</tr>
</table>

HM = Hölldobler, Manthey
DHR = Dietz, Hölldobler, Ragni

|Social Program=
We plan to do the following social activities during the summer school. Yet, the details are not fixed.

* Walking City Tour (Tuesday, 15.9.)
* Excursion to Pirna (Wednesday, 16.9.)
* Excursion to Saxon Switzerland (Saturday, 19.9.)
* Reception (together with KI 2015, Tuesday, 22.9.)
* Dinner at Eckberg Castle (Thursday, 24.9. for grant holders, academic and others; students will given free tickets if available)

|Stay in Dresden=

'''Accomodation'''

Some hotels and apartment agencies offer accommodation to participants.

All suggested places are conveniently connected by public transportation to the summer school and workshop venue.

Please act fast, because it´s very difficult to find rooms in Dresden in this period of the year. Here, we provide a list of [https://ddll.inf.tu-dresden.de/web/Accomodation/en well located and affordable accommodation].

'''Living Expenses'''

* Accommodation: The costs for accommodation depend on the place, where you book a room and can be found on the web pages linked from the page above.
* Living: For food and living no exact information can be given as this is too individual. A calculation for Saxon law amounts to 24 EUR per day.
* Public transportation: If you want to use public transports, please see [[Info and Venue]] for the ticket fares and possibilities.
* Cultural program: We don't charge any addition for our cultural program. Only for some single events you may need some little money for food etc. as mentioned on the event information pages.
* Per diems: The per diems rates for Germany given by the European Commission amount to 208 EUR. These rates include all arising costs as mentioned above.

'''Child Care'''

A flexible child care is offered to participants of congresses or other events taking place at the Technische Universität Dresden.
It gives you the possibility to take your children to Dresden and leave them under care of educated staff, when attending lectures.

For more information, please contact:

Campusbüro Uni mit Kind

George-Bähr-Straße 1b

Tel./Fax: +49-351-463-32666 / -32667

E-mail: campusbuero@tu-dresden.de

[http://kinder.studentenwerk-dresden.de/ German web page]

|Chairs and Organizers=

'''Chair of the Summer School''' [[ Steffen Hölldobler]]

'''Organizers of the Summer School''' [[Emmanuelle Dietz]], [[Julia Koppenhagen]], [[Norbert Manthey]]

}}

WVPub111

2015-04-17T07:37:11Z

Norbert Manthey:

{{Publikation Erster Autor
|ErsterAutorVorname=Davide
|ErsterAutorNachname=Lanti
|FurtherAuthors=Ahmed Irfan; Norbert Manthey
}}
{{Inproceedings
|Referiert=1
|Title=Pcasso -- a Parallel CooperAtive Sat SOlver
|To appear=0
|Year=2014
|Booktitle=Proceedings of SAT Competition 2014
|Pages=56
|Publisher=University of Helsinki, Helsinki, Finland
|Editor=Anton Belov and Daniel Diepold and Marijn J.H. Heule and Matti Järvisalo
|Series=Department of Computer Science Series of Publications B
|Volume=B-2014-2
|Organization=
}}
{{Publikation Details
|Forschungsgruppe=Wissensverarbeitung
}}

Forschungslinie (SS2015)

2015-04-13T15:46:21Z

Norbert Manthey:

Datei:Satvorstellung-Forschungslinie-SS2015.pdf

2015-04-13T15:46:14Z

Norbert Manthey: Norbert Manthey lud eine neue Version von „Datei:Satvorstellung-Forschungslinie-SS2015.pdf“ hoch

SAT-Solving und das Lösen von Sudokus (SS2015)

2015-04-13T12:54:26Z

Norbert Manthey:

Forschungslinie (SS2015)

2015-04-13T10:38:24Z

Norbert Manthey:

Datei:Satvorstellung-Forschungslinie-SS2015.pdf

2015-04-13T10:37:52Z

Norbert Manthey:

Forschungslinie (SS2015)/en

2015-04-13T08:58:48Z

Norbert Manthey: Page created automatically by parser function on page Forschungslinie (SS2015)

Forschungslinie (SS2015)

2015-04-13T08:58:47Z

Norbert Manthey: Die Seite wurde neu angelegt: „{{Vorlesung |Title=Forschungslinie |Research group=Wissensverarbeitung |Lecturers=Steffen Hölldobler; |Term=SS |Year=2015 |SWSLecture=0 |SWSExercise=0 |SWSPr…“

Thema3419/en

2015-03-03T08:26:08Z

Norbert Manthey: Page created automatically by parser function on page Thema3419

Thema3419

2015-03-03T08:26:07Z

Norbert Manthey: Die Seite wurde neu angelegt: „{{Abschlussarbeit |Titel DE=Verbinden von Suchabstraktionen zur echten Suche |Titel EN=Relating Search Abstractions to Actual Search |Abschlussarbeitstyp=Bache…“

{{Abschlussarbeit
|Titel DE=Verbinden von Suchabstraktionen zur echten Suche
|Titel EN=Relating Search Abstractions to Actual Search
|Abschlussarbeitstyp=Bachelor, Master, Diplom, Studienarbeit
|Betreuer=Norbert Manthey
|Forschungsgruppe=Wissensverarbeitung
|Abschlussarbeitsstatus=Offen
|Beschreibung DE=Moderne SAT Solver sind sehr komplexe Systeme mit vielen integrierten Techniken und Heuristiken. Um diese intuitiv zu verstehen wurde eine Abstraktion entwickelt: die Suche eines Ausgangs in einem Labyrinth. Zu den verschiedenen Situationen im Labyrinth sollen entsprechende Formeln gefunden werden, sodass sich der SAT Solver bei der Suche genau so verhält wie der Agent im Labyrinth.
|Beschreibung EN=Modern SAT solver are highly complex systems with many integrated techniques and heuristics. To make this technology available for teaching, we developed an abstraction: finding an exit in a maze. The task of this project is to find example formulas that are related to the special situations in the maze, such that a SAT solver behaves exactly like the agent in the maze.
}}

Knowledge Representation and Reasoning Seminar (SS2015)

2015-03-02T13:49:56Z

Norbert Manthey:

{{Vorlesung
|Title=Knowledge Representation and Reasoning Seminar
|Research group=Wissensverarbeitung
|Lecturers=Steffen Hölldobler;
|Term=SS
|Year=2015
|SWSLecture=0
|SWSExercise=2
|SWSPractical=0
|Exam type=mündliche Prüfung, Referat
|Description=Seminar: Montag, 2.DS

Seminar about recent research developments in SAT solving. More details will be added soon.
}}

SAT-Solving und das Lösen von Sudokus (SS2015)

2015-03-02T13:48:43Z

Norbert Manthey: