Tableau Calculi for Answer Set Programming
Speaker: Professor Torsten Schaub, University of Potsdam, Germany
When: 2006-03-30 12:30:00
Venue: N54 2.06 Nathan campus, Griffith University.
Host: Prof Abdul Sattar
Abstract:We introduce a formal proof system based on tableau methods for
analyzing computations made in Answer Set Programming (ASP). Our
approach furnishes declarative and fine-grained instruments for
characterizing operations as well as strategies of ASP-solvers:
(1) The granulation is detailed enough to capture the variety of
propagation and choice operations of algorithms used for ASP;
this also includes SAT-based approaches.
(2) It is general enough to encompass the various strategies pursued
by existing ASP-solvers. This provides us with a uniform
framework for identifying and comparing fundamental properties
of algorithms.
(3) The approach allows us to investigate the proof complexity of
algorithms for ASP, depending on choice operations. In
particular, we show that exponentially different best-case
computations can be obtained for different ASP-solvers.
(4) Our approach is flexible enough to integrate new inference
patterns, so to study their relation to existing ones. As a
result, we obtain a novel approach to unfounded set
handling. This approach is based on loops but not restricted to
SAT-based solvers, which already exploit the
concept. Furthermore, we identify backward propagation
operations for unfounded sets, which appear to be the first of
their kind.
RSVP to Natalie Dunstan by Thursday 23 March 2006
Biography:Torsten Schaub received his diploma and dissertation in informatics
in 1990 and 1992, respectively, from the Technical University of
Darmstadt, Germany. He received his habilitation in informatics in
1995 from the University of Rennes I, France. From 1990 to 1993 he
was a Researcher at the Technical University at Darmstadt. From 1993
to 1995, he was a Research Associate at IRISA/INRIA at Rennes. From
1995 to 1997, he was University Professor at the University of
Angers. At Angers he founded the research group FLUX dealing with
the automatisation of reasoning from incomplete, contradictory, and
evolutive information. Since 1997, he is University Professor for
knowledge processing and information systems at the University of
Potsdam. In 1999, he became Adjunct Professor at the School of
Computing Science at Simon Fraser University. Since 2002 Torsten
Schaub serves as head of the Institute of Informatics. His
particular research interests range from the theoretic foundations
to the practical implementation of methods for reasoning from
incomplete and/or inconsistent information.
Type: Institute for Integrated and Intelligent Systems
Contact:Prof Abdul Sattar, seminar host (n.dunstan@griffith.edu.au)
or Guido Governatori (ITEE seminar co-ordinator)
(guido@itee.uq.edu.au)