A compositional typed higher-order logic with definitions

Ingmar Dasseville, Matthias Van Der Hallen, Bart Bogaerts, Gerda Janssens, Marc Denecker

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

2 Citations (Scopus)
26 Downloads (Pure)


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.

Original languageEnglish
Title of host publicationTechnical Communications of the 32nd International Conference on Logic Programming
Subtitle of host publicationICLP 2016, October 16–21, 2016, New York City, USA
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Number of pages13
ISBN (Electronic)9783959770071
Publication statusPublished - 1 Nov 2016
MoE publication typeA4 Article in a conference publication
EventInternational Conference on Logic Programming - New York City, United States
Duration: 16 Oct 201621 Oct 2016
Conference number: 32

Publication series

NameOpen Access Series in Informatics
ISSN (Electronic)2190-6807


ConferenceInternational Conference on Logic Programming
Abbreviated titleICLP
CountryUnited States
CityNew York City


  • Compositionality
  • Logic
  • Semantics

Fingerprint Dive into the research topics of 'A compositional typed higher-order logic with definitions'. Together they form a unique fingerprint.

Cite this