Abstract
Although assertions can be combined in propositional logic, an intrinsic relationship to the primitive propositions cannot be stated. In this chapter, we introduce the first-order predicate logic with equality in which the intrinsic relationship of objects, and their attributes can be formalized. Formulas can be interpreted over structures rather than on simple values.
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
Similar content being viewed by others
References
Becker MY (2005) Cassandra: flexible trust management and its application to electronic health records. Technical report, UCAM-CL-TR-648, University of Cambridge, United Kingdom
Becker MY, Sewell P (2004) Cassandra: distributed access control policies with tunable expressiveness. In: POLICY ’04: proceedings of the fifth IEEE international workshop on policies for distributed systems and networks. IEEE Press, New York, pp 159–168
Bertot Y, Castéran P (2004) Interactive theorem proving and program development. Texts in theoretical computer science. Springer, Berlin
Bonatti PA, Shahmehri N, Duma C, Olmedilla D, Nejdl W, Baldoni M, Baroglio C, Martelli A, Coraggio P, Antoniou G, Peer J, Fuchs NE (2004) Rule-based policy specification: state of the art and future work. Technical report, Dipatimento di Scienze Fisiche, Universit a di Napoli, Complesso Universitario di Monte Sant Angelo
Chen F, Sandhu RS (1996) Constraints for role-based access control. In: RBAC ’95: proceedings of the first ACM workshop on role-based access control. ACM, New York, pp 39–46
Ceri S, Gottlob G, Tanca L (1989) What you always wanted to know about Datalog (and never dared to ask). IEEE Trans Knowl Data Eng 1(1):146–166
Clocksin WF, Mellish CS (1984) Programming in prolog using the ISO standard. Springer, New York
Davis R, Shrobe H, Szolovits P (1993) What is a knowledge representation? AI Mag 14(1):17–33
DeMarco T (1978) Structured analysis and system specification. Yourdon Press, New York
Floyd R (1967) Assigning meaning to programs. In: Mathematical aspects of computer science, XIX. American Mathematical Society, Washington, pp 19–32
Gordon MJC, Melham TF (1993) Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, Cambridge
Guaspari FD, Marceau C, Polak W (1990) Formal verification of Ada programs. IEEE Trans Softw Eng 16(9):1044–1057
Garland SJ, Guttag JV, Horning JJ (1990) Debugging Larch shared language specifications. IEEE Trans Softw Eng 16(9):1058–1075
Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576–583
Hoare CAR (1972) Proof of correctness of data representations. Acta Inform 1(1):271–281
Nipkow T, Paulson LC, Wenzel M (2002) Isabelle/HOL: a proof assistant for higher order logic, LNCS, vol 2283. Springer, Berlin
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2011 Springer-Verlag London Limited
About this chapter
Cite this chapter
Alagar, V.S., Periyasamy, K. (2011). Predicate Logic. In: Specification of Software Systems. Texts in Computer Science. Springer, London. https://doi.org/10.1007/978-0-85729-277-3_10
Download citation
DOI: https://doi.org/10.1007/978-0-85729-277-3_10
Publisher Name: Springer, London
Print ISBN: 978-0-85729-276-6
Online ISBN: 978-0-85729-277-3
eBook Packages: Computer ScienceComputer Science (R0)