Logic in computer science
From Wikipedia, the free encyclopedia
For the academic conference LICS, see IEEE Symposium on Logic in Computer Science.
Logic in computer science describes topics where logic is applied to computer science and artificial intelligence. These include:
- Investigations into logic that are guided by applications in computer science. For example:
- Combinatory logic and Abstract interpretation;
- Boolean logic, for the circuits used in computer processors.
- Logics of knowledge and beliefs (of human and artificial agents);
- Spatial logics, used for reasoning about interaction between concurrent and distributed processes.
- Logics for spatial reasoning, e.g. about moving in Euclidean space (which should not be confused with spatial logics used for concurrent systems);
- Applications of logic in computer science, such as Formal methods:
- Specification languages are extended logics for reasoning about whether programs behave correctly, such as the Z specification language. Cf. program logics, below, which can be considered to be minimalist specification logics, and cf. also, automated theorem provers, below; specification languages are often intergrated into theorem provers.
- The notion of institution has been developed as an abstract formalization of the notion of logical system, with the goal of handling the "population explosion" of logics used in formal methods.
- Predicate logic and logical frameworks are used for proving programs correct, and logics such as temporal logic and #Fundamental concepts in computer science that are naturally expressible in formal logic. For example:
- Formal semantics of programming languages,
- Program logics, such as Hoare logic, Hennessy-Milner logic, and dynamic logic
- Logic programming;
- Aspects of the theory of computation that cast light on fundamental questions of formal logic. For example: Curry-Howard correspondence and Game semantics;
- Tools for logicians considered as computer science. For example: Automated theorem proving and Model checking;
The study of basic mathematical logic such as propositional logic and predicate logic (normally in conjunction with set theory) is considered an important theoretical underpinning to any undergraduate computer science course. Higher-order logic is usually considered an advanced topic, but is important in theorem proving tools like HOL.
[edit] Books
- Mathematical Logic for Computer Science by Mordechai Ben-Ari. Springer-Verlag, 2nd edition, 2003. ISBN 1-85233-319-7.
- Logic in Computer Science: Modelling and Reasoning about Systems by Michael Huth, Mark Ryan. Cambridge University Press, 2nd edition, 2004. ISBN 0-521-54310-X.
- Logic for Mathematics and Computer Science by Stanley N. Burris. Prentice Hall, 1997. ISBN 0-13-285974-2.
[edit] External links
- Article on Logic and Artificial Intelligence at the Stanford Encyclopedia of Philosophy.
- IEEE Symposium on Logic in Computer Science (LICS)
- Draft book on Logic in Computer Science by Andrei Voronkov
 |
This logic-related article is a stub. You can help Wikipedia by expanding it. |
