Using a first-order theorem prover in the SemAnTE framework

Abstract

To allow proofs of textual entailments in the model described by Toledo et al. using a first-order automated theorem prover, we need to rewrite higher-order expressions to first-order logic. This thesis describes a rewriting algorithm that captures a certain class of natural language inferences corresponding to modifiers. It is sound, but not complete.