Applications of Logic and Algebra in Computer Science I have used logic for specification of security policies in a security model. One of my reviewers asked a question that "why did you use logic and not algebra for this purpose, and what is your justification?".
The first answer that comes to my mind is that algebra is more suitable for using in modelling the behaviour (dynamic aspects). For example for specification of security protocols. However, logic is more suitable for specification of properties (static aspects). For example for specification of the security properties we require to satisfy in a computing environment, or the security properties we desire to be satisfied in a security protocol. In other words, algebra is suitable to say HOW, but logic is suitable to say WHAT.
My questions regarding this issue are:


*

*Is my initial answer to this question correct or not?

*What are the other answers for this question

*What are the main references describing where we should use logic, and where we should use algebra in their applications in computer science?

 A: I don't like this kind of question —not yours, your referee's— it's enough for authors to solve problems, the existence of other routes that other people might prefer is besides the point, unless there is some relative disadvantage that the referee can point out.


*

*Is my initial answer to this question correct or not? — It's not what I would say.  There are plenty of approaches to handle mutability in logic, of which dynamic logic is probably the most widely applied.

*What are the other answers for this question? — I should think that in your shoes I would say something like: "The choice of logic vs. algebra is much less important than the design decisions made in formalising the specification.  This is what seemed to me to be most well suited at the time."

*What are the main references describing where we should use logic, and where we should use algebra in their applications in computer science? — I don't know of anything along the lines of what you are asking.  Blackburn, de Rijke & Venema (2001) Modal Logic talks about the similarities and differences between algebraic and model-theoretic techniques - I left with the impression that the biggest issue was whether you preferred to work with completeness theorems or representation theorems.


To say something in addition to John's answer, here was a thread on Math Overflow, Is there a relationship between model theory and category theory, that I think gives some impression on how little distance there is seen to be between algebra and logic.
A: At some level, algebra and logic are equivalent.  See Logic as Algebra by Paul Halmos and Steven Givant.
A: You may want to read about the Curry-Howard isomorphism which, for example, tells us that types in typed lambda calculus (thus in programming languages like OCaml, SML, Haskell, among others) actually are propositions in some logic formalism, and that values of these types are proofs of the corresponding propositions. It is e.g used to develop proof assistants that actually also are functional programming languages (Agda, Coq, Epigram, ...). Regarding algebra, you may want to read "Elements of Programming", by Alexander Stepanov. 
