TY  - JOUR
A1  - Hahn, Michael
A1  - Richter, Frank
T1  - Henkin semantics for reasoning with natural language
T2  - Journal of language modelling
N2  - The frequency of intensional and non-first-order definable operators in natural languages constitutes a challenge for automated reasoning with the kind of logical translations that are deemed adequate by formal semanticists. Whereas linguists employ expressive higher-order logics in their theories of meaning, the most successful logical reasoning strategies with natural language to date rely on sophisticated first-order theorem provers and model builders. In order to bridge the fundamental mathematical gap between linguistic theory and computational practice, we present a general translation from a higher-order logic frequently employed in the linguistics literature, two-sorted Type Theory, to first-order logic under Henkin semantics. We investigate alternative formulations of the translation, discuss their properties, and evaluate the availability of linguistically relevant inferences with standard theorem provers in a test suite of inference problems stated in English. The results of the experiment indicate that translation from higher-order logic to first-order logic under Henkin semantics is a promising strategy for automated reasoning with natural languages.
KW  - Henkin semantics
KW  - reasoning
KW  - reducing higher-order reasoning to first-order reasoning
Y1  - 2017
UR  - http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/43841
UR  - https://nbn-resolving.org/urn:nbn:de:hebis:30:3-438412
SN  - 2299-8470
SN  - 2299-856X
N1  - This work is licensed under the Creative Commons Attribution 3.0 Unported License. http://creativecommons.org/licenses/by/3.0/
VL  - 3
IS  - 2
SP  - 513
EP  - 568
PB  - Instytut Podstaw Informatyki (Warszawa)
CY  - Warszawa
ER  -