Integration of abductive reasoning and constraint optimization in SCIFF

Abductive Logic Programming (ALP) and Constraint Logic Programming (CLP) share the feature to constrain the set of possible solutions to a program via integrity or CLP constraints. These two frameworks have been merged in works by various authors, which developed efficient abductive proof-procedures empowered with constraint satisfaction techniques. However, while almost all CLP languages provide algorithms for finding an optimal solution with respect to some objective function (and not justanysolution), the issue has received little attention in ALP. In this paper we show how optimisation meta-predicates can be included in abductive proof-procedures, achieving in this way a significant improvement to research and practical applications of abductive reasoning. In the paper, we give the declarative and operational semantics of an abductive proof-procedure that encloses constraint optimization meta-predicates, and we prove soundness in the three-valued completion semantics. In the proof-procedure, the abductive logic program can invoke optimisation meta-predicates, which can invoke abductive predicates, in a recursive way.