Constructing a normal form for property theory
UNSPECIFIED (1997) Constructing a normal form for property theory. In: 14th International Conference on Automated Deduction (CADE-14), TOWNSVILLE, AUSTRALIA, JUL 13-17, 1997. Published in: AUTOMATED DEDUCTION - CADE-14, 1249 pp. 237-251.Full text not available from this repository.
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.
|Item Type:||Conference Item (UNSPECIFIED)|
|Subjects:||Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software|
|Series Name:||LECTURE NOTES IN ARTIFICIAL INTELLIGENCE|
|Journal or Publication Title:||AUTOMATED DEDUCTION - CADE-14|
|Number of Pages:||15|
|Page Range:||pp. 237-251|
|Title of Event:||14th International Conference on Automated Deduction (CADE-14)|
|Location of Event:||TOWNSVILLE, AUSTRALIA|
|Date(s) of Event:||JUL 13-17, 1997|
Actions (login required)