A Compositional Typed Higher-Order Logic with Definitions

Authors Ingmar Dasseville, Matthias van der Hallen, Bart Bogaerts, Gerda Janssens, Marc Denecker

Thumbnail PDF


  • Filesize: 0.53 MB
  • 13 pages

Document Identifiers

Author Details

Ingmar Dasseville
Matthias van der Hallen
Bart Bogaerts
Gerda Janssens
Marc Denecker

Cite AsGet BibTex

Ingmar Dasseville, Matthias van der Hallen, Bart Bogaerts, Gerda Janssens, and Marc Denecker. A Compositional Typed Higher-Order Logic with Definitions. In Technical Communications of the 32nd International Conference on Logic Programming (ICLP 2016). Open Access Series in Informatics (OASIcs), Volume 52, pp. 14:1-14:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Expressive KR languages are built by integrating different language constructs, or extending a language with new language constructs. This process is difficult if non-truth-functional or non-monotonic constructs are involved. What is needed is a compositional principle. This paper presents a compositional principle for defining logics by modular composition of logical constructs, and applies it to build a higher order logic integrating typed lambda calculus and rule sets under a well-founded or stable semantics. Logical constructs are formalized as triples of a syntactical rule, a semantical rule, and a typing rule. The paper describes how syntax, typing and semantics of the logic are composed from the set of its language constructs. The base semantical concept is the infon: mappings from structures to values in these structures. Semantical operators of language constructs operate on infons and allow to construct the infons of compound expressions from the infons of its subexpressions. This conforms to Frege's principle of compositionality.
  • Logic
  • Semantics
  • Compositionality


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. H. Abramson and H. Rogers. Meta-programming in logic programming. MIT Press, 1989. Google Scholar
  2. Jon Barwise and John Etchemendy. Information, infons, and inference. Situation theory and its applications, 1(22), 1990. Google Scholar
  3. Bart Bogaerts. Groundedness in logics with a fixpoint semantics. PhD thesis, Informatics Section, Department of Computer Science, Faculty of Engineering Science, June 2015. Denecker, Marc (supervisor), Vennekens, Joost and Van den Bussche, Jan (cosupervisors). URL: https://lirias.kuleuven.be/handle/123456789/496543.
  4. Weidong Chen, Michael Kifer, and David S Warren. Hilog: A foundation for higher-order logic programming. The Journal of Logic Programming, 15(3):187-230, 1993. Google Scholar
  5. Ingmar Dasseville, Matthias van der Hallen, Gerda Janssens, and Marc Denecker. Semantics of templates in a compositional framework for building logics. TPLP, 15(4-5):681-695, 2015. URL: http://dx.doi.org/10.1017/S1471068415000319.
  6. Marc Denecker, Victor Marek, and Mirosław Truszczyński. Approximations, stable operators, well-founded fixpoints and applications in nonmonotonic reasoning. In Jack Minker, editor, Logic-Based Artificial Intelligence, volume 597 of The Springer International Series in Engineering and Computer Science, pages 127-144. Springer US, 2000. URL: http://dx.doi.org/10.1007/978-1-4615-1567-8_6.
  7. Marc Denecker and Eugenia Ternovska. A logic of nonmonotone inductive definitions. ACM Trans. Comput. Log., 9(2):14:1-14:52, April 2008. URL: http://dx.doi.org/10.1145/1342991.1342998.
  8. Keith Devlin. Logic and information. Cambridge University Press, 1991. Google Scholar
  9. Wolfgang Faber, Gerald Pfeifer, and Nicola Leone. Semantics and complexity of recursive aggregates in answer set programming. Artif. Intell., 175(1):278-298, 2011. URL: http://dx.doi.org/10.1016/j.artint.2010.04.002.
  10. Paolo Ferraris. Answer sets for propositional theories. In Proceedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), pages 119-131, 2005. URL: http://dx.doi.org/10.1007/11546207_10.
  11. Michael Gelfond and Yuanlin Zhang. Vicious circle principle and logic programs with aggregates. TPLP, 14(4-5):587-601, 2014. URL: http://dx.doi.org/10.1017/S1471068414000222.
  12. Tias Guns. Declarative pattern mining using constraint programming. Constraints, 20(4):492-493, 2015. Google Scholar
  13. Yuri Gurevich and Itay Neeman. Logic of infons: The propositional case. ACM Trans. Comput. Log., 12(2):9, 2011. URL: http://dx.doi.org/10.1145/1877714.1877715.
  14. Jerry R Hobbs and Stanley J Rosenschein. Making computational sense of montague’s intensional logic. Artificial Intelligence, 9(3):287-306, 1977. Google Scholar
  15. David B. Kemp and Peter J. Stuckey. Semantics of logic programs with aggregates. In Vijay A. Saraswat and Kazunori Ueda, editors, ISLP, pages 387-401. MIT Press, 1991. Google Scholar
  16. Javier Leach, Susana Nieva, and Mario Rodríguez-Artalejo. Constraint logic programming with hereditary harrop formula. CoRR, cs.PL/0404053, 2004. Google Scholar
  17. Vladimir Lifschitz. Answer set planning. In Danny De Schreye, editor, Logic Programming: The 1999 International Conference, Las Cruces, New Mexico, USA, November 29 - December 4, 1999, pages 23-37. MIT Press, 1999. Google Scholar
  18. Victor Marek and Mirosław Truszczyński. Stable models and an alternative logic programming paradigm. In Krzysztof R. Apt, Victor Marek, Mirosław Truszczyński, and David S. Warren, editors, The Logic Programming Paradigm: A 25-Year Perspective, pages 375-398. Springer-Verlag, 1999. URL: http://arxiv.org/abs/cs.LO/9809032.
  19. Gopalan Nadathur and Dale Miller. An overview of LambdaProlog. In Fifth International Conference and Symposium on Logic Programming. MIT Press, 1988. Google Scholar
  20. Ilkka Niemelä. Logic programs with stable model semantics as a constraint programming paradigm. Ann. Math. Artif. Intell., 25(3-4):241-273, 1999. URL: http://dx.doi.org/10.1023/A:1018930122475.
  21. Nikolay Pelov, Marc Denecker, and Maurice Bruynooghe. Well-founded and stable semantics of logic programs with aggregates. TPLP, 7(3):301-353, 2007. URL: http://dx.doi.org/10.1017/S1471068406002973.
  22. Tran Cao Son, Enrico Pontelli, and Islam Elkabani. An unfolding-based semantics for logic programming with aggregates. CoRR, abs/cs/0605038, 2006. URL: http://arxiv.org/abs/cs/0605038.
  23. Shahab Tasharrofi and Eugenia Ternovska. A semantic account for modularity in multi-language modelling of search problems. In Cesare Tinelli and Viorica Sofronie-Stokkermans, editors, Frontiers of Combining Systems, 8th International Symposium, FroCoS 2011, Saarbrücken, Germany, October 5-7, 2011. Proceedings, volume 6989 of Lecture Notes in Computer Science, pages 259-274. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-24364-6_18.
  24. Shahab Tasharrofi and Eugenia Ternovska. Three semantics for modular systems. CoRR, abs/1405.1229, 2014. URL: http://arxiv.org/abs/1405.1229.
  25. Allen Van Gelder. The well-founded semantics of aggregation. In PODS, pages 127-138. ACM Press, 1992. URL: http://dx.doi.org/10.1145/137097.137854.