Higher-Order Automated Theorem Proving for Natural Language Semantics

This paper describes a tableau-based higher-order 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, firstorder 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 -calcul..