Applied Logics for Computer Science

  • Paul Gochet
  • Pascal Gribomont


Logic is intensively applied in many areas of computer science. Successful applications often lead to the question whether alternative logics could be more adequate than classical propositional and first-order logics. Not surprisingly, answering this question usually amounts to a trade-off between the expressive power of the new logic (usually stronger than the expressive power of classical logic) and its decidability properties (usually weaker). From this point of view, formal methods for program design and verification are an interesting field of applied logic and computer science since one can take advantage of the high expressive power of specific logics and also of the algorithmic tools available in classical logic; two examples will be given. We also illustrate how logic can be used directly as a programming language.


Logic Program Search Tree Logic Programming Classical Logic Mutual Exclusion 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    I. Bratko: Prolog - Programming for Artificial Intelligence (Addison-Wesley, Reading, Mass. 1990 [2nd edition])Google Scholar
  2. 2.
    K.M. Chandy, J. Misra: Parallel Program Design: A Foundation (Addison-Wesley, Reading, Mass. 1988 )Google Scholar
  3. 3.
    C.C. Chang, R.C. Lee: Symbolic Logic and Mechanical Theorem Proving ( Academic Press, New York 1973 )MATHGoogle Scholar
  4. 4.
    J.W. De Bakker, L.G.L.T. Meertens: On the Completeness of the Inductive Assertion Method’. Journal of Computer and System Sciences 11 (1975) 323357Google Scholar
  5. 5.
    E.W. Dijkstra: A discipline of programming ( Prentice Hall, New Jersey 1976 )MATHGoogle Scholar
  6. 6.
    E.W. Dijkstra (ed.): Formal Developments of Programs and Proofs ( Addison-Wesley, Reading, MA 1990 )Google Scholar
  7. 7.
    K. Doets: From Logic to Logic Programming (MIT Press, Cambridge, Mass. 1994 )Google Scholar
  8. 8.
    R. Gerth, D. Peled, M. Vardi, P Wolper: ‘Simple On-the-fly Automatic Verification of Linear Temporal Logic’. In: Proc. 15th Work. Protocol Specification, Testing, and Verification ( North-Holland, Amsterdam 1995 )Google Scholar
  9. 9.
    P. Gochet, P. Gribomont: Logique: méthodes pour l’étude des programmes ( Hermès, Paris, 1994 )Google Scholar
  10. 10.
    D.M. Goldschlag: ‘Mechanically Verifying Concurrent programs with the Boyer-Moore prover’. IEEE Trans. on Software Engineering 16 (1990) 10051023Google Scholar
  11. 11.
    E.P. Gribomont: ‘Concurrency without toil: a systematic method for parallel program design’. Sci. Comput. Programming 21 (1993) 1–56MathSciNetMATHCrossRefGoogle Scholar
  12. 12.
    E.P. Gribomont: ‘Simplification of Boolean verification conditions’. Theoret. Comput. Sci. 239 (2000) 165–185MathSciNetMATHCrossRefGoogle Scholar
  13. 13.
    E.P. Gribomont, D. Rossetto: ‘CAVEAT: technique and tool for Computer Aided Verification And Transformation’. In: Lect. Notes in Comput. Sci. 939 ( Springer, Berlin 1995 ) 70–83Google Scholar
  14. 14.
    P. Gribomont, P. Wolper: ‘Temporal logic’. In: [27], vol. 2, ch. 4Google Scholar
  15. 15.
    D. Gries: The Science of Programming ( Springer-Verlag, Berlin 1981 )MATHCrossRefGoogle Scholar
  16. 16.
    C.A.R. Hoare: ‘An axiomatic basis for computer programming’ Comm. ACM 12 (1969) 576–583MATHCrossRefGoogle Scholar
  17. 17.
    R.P. Kurshan, L. Lamport: ‘Verification of a Multiplier: 64 Bits and Beyond’. In: Lect. Notes in Comput. Sci. 697 ( Springer, Berlin, 1993 ) 166–179Google Scholar
  18. 18.
    L. Lamport: ‘An Assertional Correctness Proof of a Distributed Algorithm’. Sci. Comput. Programming 2 (1983) 175–206MathSciNetCrossRefGoogle Scholar
  19. 19.
    J.W. Lloyd: Foundations of Logic Programming (Springer-Verlag, Berlin 1987 [2nd edition])Google Scholar
  20. 20.
    J.-L. Lassez, M.J. Mahler, K. Marriott: ‘Unification revisited’. In: Foundations of Deductive Databases and Logic programming (Ed.: J. Minker, Morgan Kaufmann, Los Altos 1988 )Google Scholar
  21. 21.
    Z. Manna et al.: STEP: the Stanford Temporal Prover (Draft), Report STANCS-TR-94–1518, Stanford University, June 1994Google Scholar
  22. 22.
    G.L. Peterson: ‘Myths about the mutual exclusion problem’. Information Proc. Lett. 12 (1981) 115–116ADSMATHCrossRefGoogle Scholar
  23. 23.
    J.A. Robinson: ‘A machine-oriented logic based on the resolution principle’. Jl. ACM 12 (1965) 23–41MATHCrossRefGoogle Scholar
  24. 24.
    D.M. Russinoff: ‘A Verification System for Concurrent Programs Based on the Boyer-Moore Prover’. Formal Aspects of Computing 4 (1992) 597–611MATHCrossRefGoogle Scholar
  25. 25.
    Y. Shoam: Artificial Intelligence Techniques in Prolog ( Morgan Kaufmann, Los Altos 1994 )Google Scholar
  26. 26.
    L. Sterling, E. Shapiro: The Art of Prolog (MIT Press, Cambridge, Mass. 1994 [2nd edition])Google Scholar
  27. 27.
    A. Thayse et al.: A logical approach to artificial intelligence ( 3 vol.) (Wiley, New-York 1989, 1991 )Google Scholar
  28. 28.
    M. Vardi, P. Wolper: ‘Reasoning about Infinite Computations’. Information and Computation 115 (1994) 1–37MathSciNetMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Paul Gochet
  • Pascal Gribomont

There are no affiliations available

Personalised recommendations