9th South-East Asian Summer School on Computational Logic
From July 18 to Augus 31, 2019, we organize the 9th ICCL summer school. The summer school will be held in in Ulaanbaatar, Mongolia and is supported by the German Academic Exchange Service (DAAD).
The first summer school has been held 2005 in HUT, Vietnam and the second summer school has been held 2006 in UI Jakarta, Indonesia. The summer schools in 2007 and 2014 have been held in Vietnam and the summer schools in 2008, 2010 and 2012 have been held in Indonesia again. 2016, the summer school was held in Thailand.
The summer school 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 and workshops dedicated to specialized topics and the state of the art.
* Arrival: 18th of August * Departure: 31th of August
The summer school is held at the Mongolian University of Sciene and Technology
Automated and Cognitive Reasoning for Question Answering by Prof. rer. nat. habil. Ulrich Furbach (Universität Koblenz-Landau, Germany)
This course will cover first order calculi with a focus on hyper tableaux. The calculus rules together with a comparison to other logical systems are introduced and an extension for an efficient handling of equality is given. Various applications for a hyper-tableau-system are discussed and, in particular, the Cognitive Reasoning approach from the Corg-Project (http://corg.hs-harz.de) is presented. We present and discuss some benchmarks for commonsense reasoning (e.g. the Winograd challange and COPA) and we demonstrate together with knowledge bases like SUMO and ConceptNet the problem of managing this huge amount of knowledge. All this is presented in the context of natural language question answering, in a way that the course participants can use the tools developed within the Corg-Project within a hands-on session.
Cognitive Computational Models of Human Thinking and Reasoning by apl. Prof. Dr. Dr. Marco Ragni (Freiburg University, Germany)
Since the times of Aristotle, humans have discussed what can be regarded as an acceptable inference striving the border of formal logical inferences and a form of ’natural deduction’ humans are applying. The ability to gain new insights from given knowledge by reasoning is one of the most fundamental cognitive abilities of humans. Psychological findings show a difference between inferences drawn by humans and those drawn by formal reasoning sys- tems implementing classical logic. These differences can be found in all domains: in reasoning about relations, in reasoning about conditional statements, and in reasoning about syllo- gisms. In this course, I will first introduce several examples for each domain demonstrating specific effects in reasoning, including content effects and illusions. In a second step, different theories of reasoning will be presented and applied to the different effects. In a third step, the theory will be evaluated and differences to other theories and alternative approaches will be discussed.
Logic by Prof. Dr. rer. nat. habil. Steffen Hölldobler, Dr. rer. nat. Emmanuelle Dietz (Technische Universität Dresden, Germany)
The course gives a comprehensive introduction into propositional and first-order logic: pro- positional formulas; interpretations and models; satisfiability, falsifiability, validity, unsatis- fiability and their relations; truth tables; logical consequences; satisfiability problems (SAT); conjunctive normal form; SAT-solving; first-order formulas; substitutions; semantics. In the tutorials, participants will be asked to turn a real world problem into a SAT-problem and to solve it using state-of-the-art SAT-solvers. This shall be organized in a competition where groups of up to three students will compete against each other. The competition will be or- ganized using a digital platform, where participants can retrieve problem instances, compute their solution, and submit it for cross-checking and evaluation.
- Sudoku as a SAT Problem by Inês Lynce and Joël Ouaknine. The last constraint of the extended encoding (page 5) contains a mistake: The OR at the beginning should be replaced by an AND, and the last two ANDs schould be replaced by two ORs.
- Sudokus with an example for input and output
- bsp-sudoku-input.txt is the form of the input
- bsp-sudoku-for-SAT.cnf is a possible way on how the bsp-sudoku-input.txt can be encoded in cnf
- bsp-sudoku-SAT-sol.txt is the output of the SAT solver for the above given encoding
- bsp-sudoku-output.txt is the readable and desired output of the sudoku solution
- the sudokus folder contains sudokus of different sizes
- Sudoku Puzzles
- SAT Solver
- SAT Solver Riss and download here
- Go to /riss_505/bin
- run with ./riss yourSudokuPuzzleInCNF.cnf
- SAT Solver Glucose (how to use it, is written on the bottom of the page)
- an alternative way of installation can be found here
- SAT Solver Riss and download here
A New Cognitive Theory: Weak Completion Semantics by Prof. Dr. rer. nat. habil. Steffen Hölldobler, Dr. rer. nat. Emmanuelle Dietz (Technische Universität Dresden, Germany)
In the last 10 years we have developed a new cognitive theory. It is based on the weak completion of logic programs, the three-valued Lukasiewizc logic, abduction and revision, and has been successfully applied to adequately model various human reasoning tasks like the suppression task, the selection task, the belief bias effect, spatial reasoning as well as reasoning about conditionals. In the course we will give an in-depth introduction into the new theory as well to its applications to different human reasoning tasks. In addition we will do experiments in order to evaluate certain reasoning tasks, in particular, how humans reason with conditionals.
To compute the least fixed point of the SvL operator, you can use the following tools:
- SvL Operator with graphical user interface (edit the environment path of your computer to run swipl from command line)
- Prolog files
Answer Set Programming for Timetabling Applications by Prof. Dr.-Ing. habil. Josef Schneeberger (Fachhochschule Deggendorf, Germany)
Answer Set Programming (ASP) offers an intuitive approach for practitioners to use compu- tational logic for applications. Like other logic languages, problem descriptions have a well defined and precise semantics. Likewise, the computed results may be properly interpreted and the presence or absence of solutions can be tracked down to rules in the problem defini- tion respectively program. In addition, ASP presents a process model to implement example programs which may be refined and refactored to accomplish new application needs and subsequent changes. We start by explicating this process model and the basic steps in ASP. A program is implemented specifying a problem description and an application model. A solution is computed by a grounding and a subsequent solving step. All programming ex- amples can be followed by hands on exercises using the Potassco System. The various parts of the ASP programming language are introduced: specification of constraints and intervals, usage of negation, arithmetic operations and comparison predicates, aggregates and optimi- zation constraints. As an application domain, various problems of university timetabling are discussed and examples are implemented. Furthermore, the integration with applications in particular web applications is discussed and demonstrated.
Description Logics by PD Dr.-Ing. habil. Anni Yasmin Turhan (Technische Universität Dresden, Germany)
Description logics (DLs) are a family of knowledge representation formalism with formal semantics that allows one to represent knowledge in a declarative way. Most DLs are decidable fragments of First Order Logic. Based on their semantics, powerful reasoning services have been defined and their computation algorithms have been investigated for a range of DLs. Recently, DLs have received more attention because they are the underlying formalism for the standardized web ontology language OWL. This course will cover an introduction into the basic notions of description logics and their reasoning services. We will discuss reasoning procedures for these services and their complexity. Then, we will examine variants of DLsthat are studied in current research, such as similarity-based ones or non-monotonic ones.
You can register for the summer school here
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.
|9:00 - 09:45||Welcome||Schneeberger||Turhan||Ragni||Turhan|
|10:15 - 11:00||Hölldobler||Schneeberger||Schneeberger||Ragni||Turhan||Excursion|
|11:30 - 12:15||Ragni||Ragni||Ragni||Turhan||Schneeberger||to|
|14:00 - 14:45||Arrival||Ragni||Ragni||Excusion||Turhan||Schneeberger||Karakorum|
|15:15 - 16:00||Turhan||Hölldobler||Excursion||Schneeberger|
|16:30 - 17:30||Turhan||Excusion||Schneeberger|
|9:00 - 09:45||Furbach||HDS||Furbach||HDS||HDS|
|10:15 - 11:00||Furbach||HDS||Furbach||HDS||HDS|
|11:30 - 12:15||HDS||Furbach||HDS||Furbach||Furbach|
|14:00 - 14:45||HDS||HDS||HDS||HDS||Evaluation|
|15:15 - 16:00||Alumni||Talks by Participants||Intercultural Differences||DAAD||Farewell|
|16:30 - 17:15||Talks by Participants||Intercultural Differences||DAAD & Study Opportunities|
HDS = Hölldobler & Dietz Saldanha
* Welcome Reception * Excursion to the Mongolian University for Science and Technology * Information about funding opportunities in Germany and about studies in Germany for students from Thailand * Event about intercultural differences together with alumni from Mongolia * Selected talks from participants and alumni * Excursion to Genghis Khan Equestrian Statue in Töw-Aimag * Excusion to Qara Qorum-City with a visit to the Besuch des Erdene Zuu monastery * Evaluation of the summer school together with the lecturers and the participants* Closing banquet
Chair of the Summer School Professor Steffen Hölldobler
Organizers of the Summer School Prof. Sarantuya Tsedendamba from MUST , Professor Dr. rer. nat. habil. Steffen Hölldobler and Dr. rer. nat. Emmanuelle Dietz Saldanha from ICCL
Sponsors gefördert vom DAAD aus Mitteln des Bundesministeriums für Bildung und Forschung (BMBF)