Towards a type discipline for answer set programming. (English) Zbl 1246.68080
Berardi, Stefano (ed.) et al., Types for proofs and programs. International conference, TYPES 2008, Torino, Italy, March 26–29, 2008. Revised selected papers. Berlin: Springer (ISBN 978-3-642-02443-6/pbk). Lecture Notes in Computer Science 5497, 117-135 (2009).
Summary: We argue that it is high time that types had a beneficial impact in the field of answer set programming and in particular disjunctive Datalog as exemplified by the DLV system. Things become immediately more challenging, as we wish to present a type system for DLV-Complex, an extension of DLV with uninterpreted function symbols, external implemented predicates and types. Our type system owes to the seminal polymorphic type system for Prolog introduced by Mycroft and O’Keefe, in the formulation by Lakshman and Reddy. The most innovative part of the paper is developing a declarative grounding procedure which is at the same time appropriate for the operational semantics of ASP and able to handle the new features provided by DLV-Complex. We discuss the soundness of the procedure and evaluate informally its success in reducing, as expected, the set of ground terms. This yields an automatic reduction in size and numbers of (non isomorphic) models. Similar results could have only been achieved in the current untyped version by careful use of generator predicates in lieu of types.
For the entire collection see [Zbl 1165.68001].
For the entire collection see [Zbl 1165.68001].
MSC:
| 68N17 | Logic programming |
References:
| [1] | Baral, C.: Knowledge Representation, Reasoning and Declarative Problem Solving. CUP (2003) · Zbl 1056.68139 · doi:10.1017/CBO9780511543357 |
| [2] | Baselice, S., Bonatti, P.A., Gelfond, M.: Towards an integration of answer set and constraint solving. In: Gabbrielli, M., Gupta, G. (eds.) ICLP 2005. LNCS, vol. 3668, pp. 52–66. Springer, Heidelberg (2005) · Zbl 1165.68481 · doi:10.1007/11562931_7 |
| [3] | Bertoni, A., Mauri, G., Miglioli, P.: A characterization of abstract data as model-theoretic invariants. In: Maurer, H.A. (ed.) ICALP 1979. LNCS, vol. 71, pp. 26–37. Springer, Heidelberg (1979) · Zbl 0411.68033 · doi:10.1007/3-540-09510-1_3 |
| [4] | Buneman, P., Ohori, A.: Polymorphism and type inference in database programming. ACM Trans. Database Syst. 21(1), 30–76 (1996) · doi:10.1145/227604.227609 |
| [5] | Calimeri, F., Cozza, S., Ianni, G.: External sources of knowledge and value invention in logic programming. Ann. Math. Artif. Intell. 50(3-4), 333–361 (2007) · Zbl 1125.68026 · doi:10.1007/s10472-007-9076-z |
| [6] | Calimeri, F., Cozza, S., Ianni, G., Leone, N.: Computable functions in ASP: Theory and implementation. In: de la Banda, M.G., Pontelli, E. (eds.) ICLP 2008. LNCS, vol. 5366, pp. 407–424. Springer, Heidelberg (2008) · Zbl 1185.68150 · doi:10.1007/978-3-540-89982-2_37 |
| [7] | Van den Bussche, J., Waller, E.: Polymorphic type inference for the relational algebra. J. Comput. Syst. Sci. 64(3), 694–718 (2002) · Zbl 1015.68062 · doi:10.1006/jcss.2001.1812 |
| [8] | Ricca, F., Gallucci, L., Schindlauer, R., Dell’Armi, T., Grasso, G., Leone, N.: OntoDLV: an ASP-based system for enterprise ontologies. Journal of Logic and Computation (to appear, 2009) · Zbl 1192.68132 · doi:10.1093/logcom/exn042 |
| [9] | Gelfond, M.: Answer sets. In: van Harmelen, F., Lifschitz, V., Porter, B. (eds.) Handbook of knowledge representation, vol. 7. Elsevier, Amsterdam (2007) |
| [10] | Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: ICLP/SLP, pp. 1070–1080 (1988) |
| [11] | Hanus, M.: Horn clause programs with polymorphic types: Semantics and resolution. Theor. Comput. Sci. 89(1), 63–106 (1991) · Zbl 0741.68029 · doi:10.1016/0304-3975(90)90107-S |
| [12] | Hermenegildo, M.V., Puebla, G., Bueno, F., López-García, P.: Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor). Sci. Comput. Programming 58(1-2), 115–140 (2005) · Zbl 1076.68540 · doi:10.1016/j.scico.2005.02.006 |
| [13] | Hill, P.M., Topor, R.W.: A semantics for typed logic programs. In: Types in Logic Programming, pp. 1–62. MIT Press, Cambridge (1992) |
| [14] | Jefferey, D.: Expressive Type Systems for Logic Programming Languages. PhD thesis, The University of Melbourne (2002) |
| [15] | Lakshman, T.L., Reddy, U.S.: Typed PROLOG: A semantic reconstruction of the Mycroft-O’Keefe type system. In: ISLP, pp. 202–217 (1991) |
| [16] | Leone, N., et al.: The DLV system for knowledge representation and reasoning. ACM TOCL 7(3), 499–562 (2006) · Zbl 1367.68308 · doi:10.1145/1149114.1149117 |
| [17] | Lloyd, J.W.: Foundations of logic programming (2nd extended ed.). Springer, Heidelberg (1987) · Zbl 0668.68004 · doi:10.1007/978-3-642-83189-8 |
| [18] | Mycroft, A., O’Keefe, R.A.: A polymorphic type system for PROLOG. Artif. Intell. 23(3), 295–307 (1984) · Zbl 0543.68076 · doi:10.1016/0004-3702(84)90017-1 |
| [19] | Nadathur, G., Qi, X.: Optimizing the runtime processing of types in polymorphic logic programming languages. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS, vol. 3835, pp. 110–124. Springer, Heidelberg (2005) · Zbl 1143.68350 · doi:10.1007/11591191_9 |
| [20] | Overton, D., Somogyi, Z., Stuckey, P.J.: Constraint-based mode analysis of Mercury. In: PPDP, pp. 109–120. ACM, New York (2002) |
| [21] | Pfenning, F.: Types in logic programming. MIT Press, Cambridge (1992) |
| [22] | Simons, P., Niemelä, I., Soininen, T.: Extending and implementing the stable model semantics. Artif. Intell. 138(1-2), 181–234 (2002) · Zbl 0995.68021 · doi:10.1016/S0004-3702(02)00187-X |
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.
