A natural framework for natural language semantics: many sorted logic and Hilbert operators in type theory - Archive ouverte HAL Access content directly
Conference Papers Year : 2013

A natural framework for natural language semantics: many sorted logic and Hilbert operators in type theory

(1, 2, 3)
1
2
3

Abstract

When computing compositionally the meaning of a sentence, depicted as a logical formula, one starts from the word senses, that are partial formulae, and combines them in accordance with the parse structure. This process involves two logics. The glue logic which combines the partial formulae: this is a lambda calculus, the lambda terms being intuitionistic propositional proofs—in Montague semantics, this logic is simply typed lambda calculus over two types, entities and truth-values (or propositions). Let us call target logic the other logic; its formulae are used to represent the meaning of the sentence—the target logic usually is higher order or first order logic. Our framework makes use of second order lambda calculus (system F) as the glue logic and many-sorted higher order logic as the target logic. The motivation for having many base types is to model restrictive selection (to leave out sentences like “The table whistles.”, to accept one like “Liverpool is an important harbour and votes labour.” (location/people) and to reject “Liverpool is an important harbour and won eighteen League titles. (location/football club). Those many base types (or sorts) naturally lead to quantify over types in order to factor operations that act uniformly over types. In such a setting, it is fairly natural to use typed Hilbert operators to express (generalised) quantification. Here we enrich our type system with predefined types, e.g., finite and countable sets (encodings in F are rather dull) and coercive subtyping (which is welcome for representing ontological inclusions like “cars” are “vehicles”) and adapt Hilbert operators to this extended type system.
Vignette du fichier
retore_logic_colloquium_2013_july26.pdf (2.11 Mo) Télécharger le fichier
Format : Presentation
Origin : Files produced by the author(s)

Dates and versions

hal-01044820 , version 1 (20-07-2019)

Identifiers

  • HAL Id : hal-01044820 , version 1

Cite

Christian Retoré. A natural framework for natural language semantics: many sorted logic and Hilbert operators in type theory. European Conference on Logic : Logic Colloquium 2013, Association for Symbolic Logic (ASL), Jul 2013, Évora, Portugal. ⟨hal-01044820⟩
245 View
4 Download

Share

Gmail Facebook Twitter LinkedIn More