|
TITLE: Tableau Calculi for Answer Set Programming
PRESENTER: Torsten Schaub, http://www.cs.uni-potsdam.de/~torsten/, torsten@cs.uni-potsdam.de
AFFILIATION:Institute of Informatics, University of Potsdam, http://www.cs.uni-potsdam.de/
DATE: Thursday 14th September 2006
TIME: 12:00:00
PLACE: CSE Seminar Room, Level 1, K17
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. First, 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.
Second, 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.
Third, the approach allows us to investigate the proof complexity
of algorithms for ASP, depending on choice operations. We show that
exponentially different best-case computations can be obtained for
different ASP-solvers. Finally, 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 based on loops, being applicable to non-SAT-based solvers.
Furthermore, we identify backward propagation operations for unfounded sets.
BIOGRAPHY OF SPEAKER:
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,
ontradictory, 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. And since 2006
he is also an Adjunct Professor at Griffiths University. His particular
research interests range from the theoretic foundations to the practical
implementation of methods for reasoning from incomplete and/or
inconsistent information.
Seminar information is also available at
http://www.cse.unsw.edu.au/db/ai/seminars/list/index.html
Host:
Toby Walsh
Seminar Convenor:
Van Hai Ho
|
