Tabling with Sound Answer Subsumption. Issue 5 (14th October 2016)

• Record Type: Journal Article
• Authors: VANDENBROUCKE, ALEXANDER; PIRÓG, MACIEJ; DESOUTER, BENOIT; SCHRIJVERS, TOM
• Editors: Carro, Manuel; King, Andy
• Is Part Of: Theory and practice of logic programming. Volume 16:Issue 5/6(2016)
• Page Start: 933
• Page End: 949
• Publication Date: 2016-10-14
• Subjects: tabling, -- answer subsumption, -- lattice, -- partial order, -- mode-directed tabling, -- denotational semantics, -- Prolog; Logic programming -- Periodicals; Artificial intelligence -- Computer programs -- Periodicals; Constraint programming (Computer science) -- Periodicals; 005.115
• DOI: 10.1017/S147106841600048X
• Languages: English
• ISSNs: 1471-0684

Abstract

Abstract: Tabling is a powerful resolution mechanism for logic programs that captures their least fixed point semantics more faithfully than plain Prolog. In many tabling applications, we are not interested in the set of all answers to a goal, but only require an aggregation of those answers. Several works have studied efficient techniques, such as lattice-based answer subsumption and mode-directed tabling, to do so for various forms of aggregation. While much attention has been paid to expressivity and efficient implementation of the different approaches, soundness has not been considered. This paper shows that the different implementations indeed fail to produce least fixed points for some programs. As a remedy, we provide a formal framework that generalises the existing approaches and we establish a soundness criterion that explains for which programs the approach is sound.