Using a first-order theorem prover in the SemAnTE framework
Benno Kruit · Utrecht University Repository (Utrecht University) · 2013
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.