×

Tabling with sound answer subsumption. (English) Zbl 1379.68084

Summary: 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.

MSC:

68N17 Logic programming
68Q55 Semantics in the theory of computing

Software:

XSB; B-Prolog; YAP-Prolog
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] AbramskyS. and HankinC.1987. Abstract Interpretation of declarative languages. Vol. 1. Ellis Horwood, Chapter An introduction to abstract interpretation, 63-102.
[2] AptK. R., BlairH. A. and WalkerA.1988. Towards a Theory of Declarative Knowledge. Morgan Kaufmann.
[3] BackhouseR. C.2000. Galois connections and fixed point calculus. In Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, International Summer School and Workshop, Oxford, UK, April 10-14, 2000, Revised Lectures, R. C.Backhouse, R. L.Crole, and J.Gibbons, Eds. LNCS, vol. 2297. Springer, 89-148.
[4] Chico de GuzmánP., CarroM., HermenegildoM. V., SilvaC. and RochaR.2008. An improved continuation call-based implementation of tabling. In Practical Aspects of Declarative Languages, 10th International Symposium. LNCS, vol. 4902. Springer, 197-213.
[5] CousotP. and CousotR.1992. Abstract interpretation and application to logic programs. The Journal of Logic Programming13, 2-3, 103-179.10.1016/0743-1066(92)90030-7 · Zbl 0776.68024 · doi:10.1016/0743-1066(92)90030-7
[6] GuoH.-F. and GuptaG.2004. Simplifying dynamic programming via tabling. In Practical Aspects of Declarative Languages. LNCS, vol. 3057. Springer, 163-177.
[7] GuoH.-F. and GuptaG.2008. Simplifying dynamic programming via mode-directed tabling.Software: Practice and Experience38, 1, 75-94.
[8] KorteB., LovászL. and SchraderR.1991. Greedoids, algorithms and combinatorics, vol. 4.
[9] LloydJ. W.1984. Foundations of Logic Programming. Springer-Verlag, New York. · Zbl 0547.68005
[10] MacNeilleH. M.1937. Partially ordered sets. Transactions of the American Mathematical Society, 416-460.
[11] OxleyJ. G.1992. Matroid theory. Oxford University Press.
[12] RamakrishnaY. S., RamakrishnanC. R., RamakrishnanI. V., SmolkaS. A., SwiftT. and WarrenD. S.1997. Computer Aided Verification: 9th International Conference, Haifa, Israel, June 22-25, 1997 Proceedings. Springer, 143-154.
[13] SantosJ. and RochaR.2013. On the efficient implementation of mode-directed tabling. In Practical Aspects of Declarative Languages. LNCS, vol. 7752. Springer, 141-156.
[14] Santos CostaV., RochaR. and DamasL.2012. The YAP Prolog system.Theory and Practice of Logic Programming12, 1-2, 5-34.10.1017/S1471068411000512 · Zbl 1244.68017 · doi:10.1017/S1471068411000512
[15] SwiftT.1999. Tabling for non-monotonic programming.Annals of Mathematics and Artificial Intelligence25, 3-4, 201-240.10.1023/A:1018990308362 · Zbl 0940.68025 · doi:10.1023/A:1018990308362
[16] SwiftT. and WarrenD.2010. Tabling with answer subsumption: Implementation, applications performance. 300-312.
[17] SwiftT. and WarrenD. S.2012. XSB: Extending Prolog with tabled logic programming.Theory and Practice of Logic Programming12, 1-2 (Jan.), 157-187.10.1017/S1471068411000500 · Zbl 1244.68021 · doi:10.1017/S1471068411000500
[18] Van HentenryckP., DegimbeO., CharlierB. L. and MichelL.1993. Abstract interpretation of Prolog based on OLDT resolution. Tech. rep., Providence, RI, USA.
[19] VandenbrouckeA., SchrijversT. and PiessensF.2016. Fixing non-determinism. In Proceedings of the 27th symposium on Implementation and Application of Functional Languages 2015.
[20] ZhouN.-F.2012. The language features and architecture of B-Prolog.Theory and Practice of Logic Programming12, 1-2, 189-218.10.1017/S1471068411000445 · Zbl 1244.68024 · doi:10.1017/S1471068411000445
[21] ZhouN. F. and DovierA.2011. A tabled Prolog program for solving sokoban. In 2011 IEEE 23rd International Conference on Tools with Artificial Intelligence. 896-897.
[22] ZhouN.-F., KameyaY. and SatoT.2010. Mode-directed tabling for dynamic programming, machine learning, and constraint solving. In 22nd International Conference on Tools with Artificial Intelligence (ICTAI), 2010. Vol. 2. 213-218.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.