摘要：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 rea_soning 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 compu?tational 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 al?ternative formulations of the translation,discuss their properties,and evaluate the availability of linguistically relevant inferences with stan?dard 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.
关键词：Henkin semantics;reasoning;reducing higher-order reasoning to first-order reasoning
