Predicate Logic

  • V. S. Alagar
  • K. Periyasamy
Part of the Texts in Computer Science book series (TCS)


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.


Policy Language Propositional Logic Predicate Logic Predicate Symbol Universal Quantifier 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    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 Google Scholar
  2. 2.
    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 Google Scholar
  3. 3.
    Bertot Y, Castéran P (2004) Interactive theorem proving and program development. Texts in theoretical computer science. Springer, Berlin MATHCrossRefGoogle Scholar
  4. 4.
    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 Google Scholar
  5. 5.
    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 Google Scholar
  6. 6.
    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 CrossRefGoogle Scholar
  7. 7.
    Clocksin WF, Mellish CS (1984) Programming in prolog using the ISO standard. Springer, New York CrossRefGoogle Scholar
  8. 8.
    Davis R, Shrobe H, Szolovits P (1993) What is a knowledge representation? AI Mag 14(1):17–33 Google Scholar
  9. 9.
    DeMarco T (1978) Structured analysis and system specification. Yourdon Press, New York Google Scholar
  10. 10.
    Floyd R (1967) Assigning meaning to programs. In: Mathematical aspects of computer science, XIX. American Mathematical Society, Washington, pp 19–32 CrossRefGoogle Scholar
  11. 11.
    Gordon MJC, Melham TF (1993) Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, Cambridge MATHGoogle Scholar
  12. 12.
    Guaspari FD, Marceau C, Polak W (1990) Formal verification of Ada programs. IEEE Trans Softw Eng 16(9):1044–1057 CrossRefGoogle Scholar
  13. 13.
    Garland SJ, Guttag JV, Horning JJ (1990) Debugging Larch shared language specifications. IEEE Trans Softw Eng 16(9):1058–1075 CrossRefGoogle Scholar
  14. 14.
    Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576–583 MATHCrossRefGoogle Scholar
  15. 15.
    Hoare CAR (1972) Proof of correctness of data representations. Acta Inform 1(1):271–281 MATHCrossRefGoogle Scholar
  16. 16.
    Nipkow T, Paulson LC, Wenzel M (2002) Isabelle/HOL: a proof assistant for higher order logic, LNCS, vol 2283. Springer, Berlin MATHGoogle Scholar

Copyright information

© Springer-Verlag London Limited 2011

Authors and Affiliations

  1. 1.Dept. Computer Science and Software Eng.Concordia UniversityMontrealCanada
  2. 2.Computer Science DepartmentUniversity of Wisconsin-La CrosseLa CrosseUSA

Personalised recommendations