Many tests of semantic properties that linguists use in their everyday life rely on reasoning. For example, if you know that all space aliens love chocolate, and you learn that Mary is a space alien, then you also know that Mary loves chocolate. This does not only tell you something important about space aliens, on closer inspection and after some serious linguistic analyzing it also reveals certain properties of the meaning of the determiner all.

If you now want to test your understanding of the semantics of English in a grammar implementation with access to reasoning systems, you will soon run into difficulties. Difficulties that occur even if you know how to program, that is. One really obnoxious problem is that well-developed logical reasoners hardly go beyond first-order predicate logic, whereas semanticists typically employ much more expressive higher-order logics in their descriptions of meaning in natural languages like English. That means that with off-the-shelf reasoners you can capture the behavior of quantifiers like all and the statements about the culinary preferences of space aliens in general and of Mary in particular, but a treatment of intensional predicates such as the verb expressing your knowledge about space aliens and Mary and your resulting knowledge about Mary’s dietary inclination are beyond these standard tools.

This is clearly not a satisfying state of affairs! In their recent paper on Henkin Semantics for Reasoning with Natural Language Michael Hahn and Frank Richter suggest a solution by defining a Henkin semantics for one of the popular higher-order logics for the description of meaning in natural languages, translating the higher-order meaning representations of linguists into first-order logic based on that semantics, and testing the performance of the resulting architecture on a set of reasoning problems stated in English.

Can we finally automatically reason about our knowledge of space aliens? Yes, we can.