Higher-Order Automated Theorem Proving for Natural Language Semantics

. This paper describes a tableau-based higherorder theorem prover Hot and an application to natural language semantics. In this application, Hot is used to prove equivalences using world knowledge during higher-order unification (HOU). This extended form of HOU is used to compute the licensing conditions for corrections. 1 Introduction Mechanized reasoning systems have many applications in Computational Linguistics. Based on the observation that some phenomena of natural language can be modeled as deductive processes, first-order theorem provers or related inference systems have been used for instance in phonology [2], generation [17] and semantic analysis [22]. [11] describes an abductive framework for natural language understanding that includes world knowledge into the semantics construction process. Other approaches use higher-order logics and in particular fi-reduction and higher-order unification (HOU) as inference procedures. Following Montague [18] who has used the typed -..