Alix Ramsay Davis

This paper presents a theorem prover for a highly intensional logic, namely a constructive version of property theory [25] . The paper presents the basic theorem prover, which is a higher-order extension of Manthey and Bry's model generation theorem prover for first-order logic [14]; considers issues relating to the compile-time optimisations that are often used with first-order theorem provers; and shows how the resulting system can be used in a natural language understanding system