TY - JOUR AU - Hahn, Michael AU - Richter, Frank PY - 2016/02/11 Y2 - 2024/03/28 TI - Henkin semantics for reasoning with natural language JF - Journal of Language Modelling JA - JLM VL - 3 IS - 2 SE - Articles DO - 10.15398/jlm.v3i2.113 UR - https://jlm.ipipan.waw.pl/index.php/JLM/article/view/113 SP - 513–568 AB - 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.<br /><br /><span class="im">The paper is accompanied by the source code (cf. <a href="/index.php/JLM/article/view/113/122">SUPP. FILES</a>) of the </span>grammar and reasoning architecture described in the paper. ER -