The theory of Answer Set Programming
Answer Set Programming (ASP) is the realisation of much theoretical work on Non-monotonic Reasoning and AI applications. It represents a new paradigm for logic programming that allows, using the concept of negation as failure, to handle problems with default knowledge and produce non-monotonic reasoning.
Two popular software implementations to compute answer sets are dlv and smodels. The efficiency of such programs allowed to increase the list of practical applications in the areas of planning, logical agents and artificial intelligence. The original definition of answer sets for disjunctive logic programs was given by Gelfond and Lifschitz (1988). It was later generalised by Lifschitz, Tang and Turner (1999) to handle the class of nested logic programs.
Our results in this line of research intend, mostly, to study properties and characteristics of answer sets in terms of non-classical logics, in particular intuitionistic and Gödel multivalued logics. This approach to study answer sets was initiated with a result from Pearce that offered a characterisation of answer sets for disjunctive logic programs in terms of intuitionistic logic.
One of our results was to generalise this characterisation in order to deal with nested logic programs [tplp04]. Our proof is based, in fact, on another important result we provided, that is a transformation of nested logic programs into standard disjunctive ones [lopstr01]. We have also proved the invariance with respect to the background logic [wollic02]. We can use, instead of intuitionistic logic, any other intermediate logic and the result still holds. Based on these results we proposed a general framework to study the answer set semantics in terms of, what we called, consistent neg-extensions [lc02].
A particular logic that was found to be useful is G3, the 3-valued logic defined by Gödel. Generalising a result given by Lifschitz, Pearce and Valverde (2001) we have shown that this logic of G3 characterises the notion of strong equivalence [esslli02] between logic programs. A remarkable fact of this result is that it was proved without depending on the syntax of formulas, so it is not only valid in the context of nested logic programs but a little beyond (arbitrary propositional formulas).
Other results deal with ideas on how to define, based again on G3, some sort of weak answer set semantics with debugging purposes [iclp02]. We have been discussing on how to use this weak semantics to find undefined atoms and detect violated constraints within logic programs. Thus giving the logic programmer some pointers on where possible mistakes could be found.
More recent results were focused on the study of properties of translations for logic programs [esslli03]. We have presented, in particular, a polynomial translation that can be used to reduce any propositional theory into the class of disjunctive logic programs. Some other interesting properties and attributes of translation in the context of answer sets were found. Examples are the property that theories can be extended by adding definitions and some relations between syntactical and semantical properties of translations.
You can check my list of publications in this and some related topics, or find more information at the site of the research group.