RPE: Amelia Harrison, Thursday, May 1, 10:00 am, GDC 3.816

Contact Name: 
Lydia Griffith
May 1, 2014 10:00am - 12:00pm

RPE: Amelia Harrison

date: Thursday, May 1, 2014
time: 10:00 am
place: GDC 3.816
committee members: Warren Hunt (chair), Ray Mooney, and Greg Plaxton

title: Proving Strong Equivalence of Answer Set Programs

Answer Set Programming (ASP) is a declarative approach to solving
combinatorial search problems, based on the concept of a stable
model. We can view a traditional answer set program as a set of
propositional formulas and define the semantics of the program in terms
of this set. There is a rich body of theoretical work for reasoning about
traditional programs. The theory of strong equivalence is an example of
such work. Two ASP programs are strongly equivalent if they can be
interchanged within the context of any larger program without affecting
the program's meaning. Strong equivalence is an important concept in
ASP because it allows us to perform local optimizations on programs.

The theory of strong equivalence was originally developed based on
the translation of programs to propositional formulas. However, as ASP
has grown in popularity, new constructs have  been added to input languages
which cannot, in general, be represented using propositional formulas.
Infinitary propositional formulas can be used to represent a more general
class of ASP programs. In this work, we describe how to extend the
theory of strong equivalence to infinitary propositional formulas.