Henkin Semantics for Reasoning with Natural Language (bibtex)

by **Michael Hahn**, Frank Richter

Abstract:

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.

Reference:

Henkin Semantics for Reasoning with Natural LanguageMichael Hahn, Frank RichterJournal of Language Modeling, 2015.

Bibtex Entry:

@Article{hahn_henkin_2015, author = {Michael Hahn and Richter, Frank}, title = {Henkin {Semantics} for {Reasoning} with {Natural} {Language}}, journal = {Journal of Language Modeling}, year = {2015}, volume = {3}, number = {2}, pages = {513--568}, png = {figs/henkin.png}, URL = {http://jlm.ipipan.waw.pl/index.php/JLM/article/view/113}, github = {https://github.com/m-hahn/henkin}, abstract = {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.} }

Powered by bibtexbrowser