Rina Dechter - Constraint Processing

Contents (provisional):

Introduction

The constraint network model,

Graph representations,

The two primary paradigms of inference + search.

Inference - consistency algorithms:

local-consistency vs. global-consistency,

arc and path-consistency,

directional-consistency,

adaptive-consistency,

relational-consistency,

bucket-elimination.

Search with Backtracking:

Look-ahead schemes: forward-checking, variable and value orderings, constraint propagation.

The Davis-Putnam algorithm.

Look-back schemes: backjumping, constraint learning.

Combining search and inference; the cycle-cutset scheme.

(If time permits, selection from):

Stochastic local search (SLS, GSAT, WSAT),

constraint optimization and probabilistic constraints.

Temporal constraint networks

Patrick Cousot - Abstract Interpretation: Theory and Applications

Semantic foundations of program analysis.

Abstract Interpretation Based Formal Methods and Future Challenges.

Veronica Dahl - Logic Programming for Computational Linguistics and Intelligent Systems

Introduction

Computational linguistics

Logic grammars

Representing meaning

Main problems in syntax

Approaches to unbounded movement

Querying from NL

Programming through NL

Some web-oriented applications

Information extraction

Virtual worlds

Concept-based classifications

Bart Demoen - Topics in Logic Programming Implementation

Implementation of Prolog

The WAM and variants for pure Prolog

The implementation of forward execution

Term representation and unification

The implementation of backtracking

Optimizations

Indexing

...

Actual systems

The implementation of some ISO extensions to pure Prolog

Cut

Assert/retract

Arithmethic

Exception handling

...

The implementation of some non-ISO extensions to Prolog

Co-routining

Attributed variables

Constraints

Using static information for performance

Discussion

Memory management of Prolog

Usefulness logic

Environment and choice point trimming

Overflow checking

A sliding collector for the WAM

A copying collector for the WAM

Variable shunting

Discussion

Memoization and Prolog

The what and why of memoization in LP

Implementations of memoization

The control flow

SLGWAM

Dynamic reordering ...

Linear tabling

The notion of completion

The tables

Tries

Some optimisations

Memory management and memoization

Javier Esparza - Model Checking of Finite and Infinite State Systems

Basics

A bit of history

A case study: the Needham-Schroeder protocol

Linear and branching time temporal logics

Model-checking LTL

The automata-theoretic approach

On-the-fly model checking

Partial-order techniques

Model-checking CTL

Basic algorithms

Binary Decision Diagrams

Infinite state spaces

Sources of infinity

Symbolic search

Accelerations and widenings

Nicola Leone - Disjunctive Logic Programming: Knowledge Representation Techniques, Systems, and Applications

Theoretical Foundations

Semantics

Program's Properties

Computational Complexity

Expressive Power

Evaluation's Algorithms

Intelligent Instantiation

Model Generation

Model Checking

Heuristics

Knowledge Representation and Applications

Declarative Programming Methodology

Application to Information Integration, Knowledge Management, Planning, and Diagnosis

Application Front-ends

Systems

DLV

GnT/Smodels

Demos

Exercises on the practical usage of DLP systems for representing and solving advanced knowledge-based problems.