Efficient Reductants Calculi using Partial Evaluation Techniques with Thresholding 1

Reductants are a useful theoretical tool introduced for proving correctness properties in the context of generalized annotated logic programming. This concept was adapted to the more recent and flexible framework of multi-adjoint logic programming for solving a problem of incompleteness that arises when working with some lattices. In order to be complete, multi-adjoint logic programs must be extended with their set of reductants. In general, the notion of reductant may introduce an important efficiency drawback. In this work we provide a more refined version of this concept that we call PE-reductant, by using (threshold) partial evaluation techniques. Our proposal is intended to be semantically equivalent to the classical notion of reductant, and improves previous approaches at least in the following two efficiency criteria. Firstly, using the new definition of reductant, we can obtain computed answers for a given goal with a lesser computational effort than by using its precedent ones. Secondly, the proper construction of a reductant by means of partial evaluation methods, is drastically improved after introducing thresholding techniques which dynamically reduce the size of the underlying unfolding trees.