THEOREM-PROVING FOR INTENSIONAL LOGIC

For a number of tasks in knowledge representation, and particularly in natural language semantics, it is useful to be able to treat propositions and properties as objects - as items that can appear as arguments of predicates, as things one can quantify over, and so on. Logics that support such ''intensional'' operations are notoriously hard to work with. The current paper presents a theorem prover for one such logic, namely, Turner's property theory.