Modular Answer Set Programming

In answer set programming (ASP) a problem is solved declaratively by writing down a logic program the answer sets of which correspond to the solutions of the problem, and computing the answer sets of the program using a special purpose search engine.The growing interest towards ASP is mostly due to efficient search engines, such as

smodels

and

dlv

. Consequently, a variety of interesting applications of ASP has emerged, e.g., in planning, product configuration, and computer aided verification.Despite the declarative nature of ASP the development of programs resembles that of programs in conventional programming, i.e., a programmer often develops a series of programs for a particular problem, e.g., when optimizing execution time and space.This gives rise to a meta-level problem of verifying whether subsequent programs are equivalent. To solve the equivalence verification problem a translation-based approach has been proposed and extended further [1,2,3] . The idea is to combine logic programs

P

and

Q

into logic programs EQT(

P

,

Q

) and EQT(

Q

,

P

) which have no answer sets iff

P

and

Q

are equivalent, which allows the use of the same ASP solver for the equivalence verification task as for the search of answer sets. The translation-based method treats programs as integral entities which limits its usefulness, e.g., if a small local change is made in a large program. The same line of thinking applies to current ASP methodology in general. ASP programs are typically seen as integral entities, and there is a lack of mechanisms available in modern programming languages that ease program development by allowing re-use of code or breaking programs into smaller pieces.