Constructing a normal form for property theory

Abstract

Property Theory, introduced in [Turner 87], is a classical first-order logic that includes a ⋅ operator to turn propositions, properties and relations into terms. It is therefore an appropriate representation language for intensional concepts such as knowledge and belief. The main advantage of Property Theory over languages like Montague semantics is that it is a type-free language, and hence provides considerable extra expressive power. The pay-back is that it is consequently extremely intractable, and constructing an appropriate normal form has proven to be very difficult. [Ramsay 95] has already presented a preliminary model generation theorem prover for Property Theory, based on the SATCHMO algorithm for predicate calculus ([Manthey 88]). However, [Ramsay 95] does not construct a satisfactory normal form for Property Theory. In this paper we examine and extend the model theory of Property Theory and present a normal form based on our extension of Property Theory. We conclude by outlining the role of our normal form in a model generation theorem prover for Property Theory.