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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
A theorem prover for Property Theory, by Mary Cryan; MSc thesis, University College Dublin, 1995.
Introduction to Montague semantics, by David Dowty, Robert E. Wall and Stanley Peters; 1981
“Notes on naive semantics”, by Hans G. Herzberger; in Journal of Philosophical Logic, Vol 11, 1982
“SATCHMORE: SATCHMO with RElevancy”, by Donald W. Loveland, David D. Reed and Debra S. Wilson; in Journal of Automated Reasoning, Vol 14, 1995
“SATCHMO: A Theorem Prover in PROLOG”, by Rainer Manthey and Francois Bry; in the 9th International Conference on Automated Deduction, Springer-Verlag, 1988
“A formal theory of knowledge and action”, by Robert Moore; in Formal theories of the commonsense world, eds. J.R. Hobbs and R.C. Moore, Ablex Pub. Corp., New Jersey, 1984
Formal Methods in Artificial Intelligence, by Allan Ramsay; Cambridge University Press, 1988
“Generating Relevant Models”, by Allan Ramsay; in Journal of Automated Reasoning, Vol 7, 1991
“Bare Plural NPs and Habitual VPs”, by Allan Ramsay; in Proceedings of the 14th International Conference on Computational Linguistics (COLING-94), 1992
“Theorem Proving for Intensionsl Logic”, by Allan Ramsay; in Journal of Automated Reasoning, Vol 14, 1995
“A Theory of Properties”, by Ray Turner; in Journal of Symbolic Logic, Vol 52(2), 1987
Truth and Modality for Knowledge Representation, by Ray Turner; Pitman, London, 1990
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cryan, M., Ramsay, A. (1997). Constructing a normal form for Property Theory. In: McCune, W. (eds) Automated Deduction—CADE-14. CADE 1997. Lecture Notes in Computer Science, vol 1249. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63104-6_22
Download citation
DOI: https://doi.org/10.1007/3-540-63104-6_22
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63104-0
Online ISBN: 978-3-540-69140-2
eBook Packages: Springer Book Archive