A natural framework for natural language semantics: many sorted logic and Hilbert operators in type theory - Méthodes et Ingénierie des Langues, des Ontologies et du Discours Accéder directement au contenu
Communication Dans Un Congrès Année : 2013

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

Résumé

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.

Mots clés

retore_logic_colloquium_2013_july26.pdf (2.11 Mo) Télécharger le fichier
Format : Présentation
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

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

Identifiants

  • HAL Id : hal-01044820 , version 1

Citer

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⟩
257 Consultations
5 Téléchargements

Partager

Gmail Facebook X LinkedIn More