Speakers
ISCL 2011 is proud to announce among its speakers:
- Giorgio Delzanno, University of Genova, Italy
- Enrico Franconi, Free University of Bozen-Bolzano, Italy
- Robert Kowalski, Imperial College London, UK
- Dale Miller, INRIA Saclay, France
- Pascal Van Hentenryck, Brown University, US
Topics
ISCL 2011 will propose courses on the following topics (click on course title to show abstract):
- Constraint Languages for Parametrized Verification: Bags, Words, Trees, and Graphs
Parametrized verification is aimed at developing methods for proving the correctness of systems consisting of an arbitrary number of repeated components. In the lectures we overview some of the methods that can be applied to systems in which configurations can be represented by structures like bags, words, trees, and graphs. Examples of this class of systems are:
• broadcast protocols (used to model cache coherence protocols),
• automata with global conditions (used to model mutual exclusion protocols for N-processes),
• tree rewriting systems (used to model hierarchical systems),
• selective broadcast protocols (used to model protocols for ad hoc networks).
In the presentation we use the metaphor "constraints as symbolic representation of sets of states" to give a uniform presentation of verification methods and of termination conditions in all these types of systems. Prerequisites: Basics of logic and algorithms. (Lecturer: Giorgio Delzanno). - Description Logics
The main effort of the research in knowledge representation is providing theories and systems for expressing structured knowledge and for accessing and reasoning with it in a principled way. In this course we will study Description Logics (DL), an important powerful class of logic-based knowledge representation languages, which also form the logical underpinning of the OWL family of web ontology languages standardised by W3C. The emphasis will be on a rigorous approach to knowledge representation and building ontologies. DL will be introduced with its simplest formalization; the computational properties and algorithms of the so called structural DL will be analysed. Then, the course considers propositional DL: we will study the computational properties and the reasoning with tableaux calculus. In the final part of the course, we will consider advanced topics such as the representation of knowledge bases and ontologies, and the connections of DL with database theory.
(Lecturer: Enrico Franconi). [course Home Page] - Computational Logic and Human Thinking: How to be Artificially Intelligent
This course is based on the book Computational Logic and Human Thinking: How to be Artificially Intelligent to be published by Cambridge University Press.
In both this course and the book, I make the case for a comprehensive, logic-based theory of human intelligence, drawing upon and reconciling a number of otherwise competing paradigms in Artificial Intelligence and other fields. The most important of these paradigms are production systems, logic programming, classical logic and decision theory. The technical foundations of the theory are provided by abductive logic programming embedded in an observation-thought-decision-action agent cycle. The theory draws support, not only from Logic, Computing and Artificial Intelligence, but from related developments in Cognitive Psychology, Philosophy, Law and Management Science. (Lecturer: Robert Kowalski). - Unity in Computational Logic
Computational logic is divided into several different fragments.
There is the division between the proof-as-program (functional
programming) approach and the proof-search (logic programming)
approach to specifying computation. There is the division among
computation, model checking, and theorem proving. Even at the level
of the description of such technical devices as proofs systems, there
is the division among sequent calculus, natural deduction, tableaux,
and resolution. In these lectures, I will show how recent results in
structural proof theory bring an organization to these topics so that
these divisions can be understood as certain choices within a large,
flexible framework. That framework involves recent lessons learned
from linear logic, focused proofs systems, and the use of fixed points
and equality as logical connectives. (Lecturer: Dale Miller). - Constraint Programming and Optimization Systems
Constraint programming is a declarative paradigm for expressing and solving hard combinatorial optimization problems. Constraint programming features an expressive and compositional language for expressing constraints, which captures substructures on an application. Moreover, constraint programming typically offers a rich search language to guide the solver towards feasible and infeasible solutions. Computationally, constraint programming uses constraints to filter infeasible values from the variable domains. This course reviews both of these aspects, explores the hybridization of constraint programming with other optimization paradigms, and discusses similarities and differences with other approaches to optimization and constraint satisfaction. Real case studies in a modern constraint programming languages demonstrate the technology.
(Lecturer: Pascal Van Hentenryck).
Schedule & Activities
A tentative schedule is available. The programme will include:
- an introductory lecture to provide an overview of the school
- 5 topical courses of 6 hours each
- brainstorming sessions over dinner
- a student session and mentoring activities
- a social trip
The school will organize student examinations, on demand. For Italian students, the participation to all courses and successful result of the examination will correspond to 2 CFU.
DALT School 2011
Registration to ISCL 2011 will grant bonus access to all courses of the co-located First International School on Declarative Agent Languages and Technologies.