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:
- Rewriting systems were motivated by solving equations algorithmically;
- Many developments in type theory were motivated by applications in programming language theory;
- Abstract interpretation was developed to allow proofs of certain program properties;
- 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);
- some developments in categorical logic;
- Program logics, such as Hoare logic, Hennessy-Milner logic, and dynamic logic are used to reason about program correctness
- Process calculi were developed to reason about correctness of concurrent systems.
- Descriptive complexity theory relates logics to computational complexity
- Applications of logic in computer science, such as Formal methods:
- Boolean logic, is used for the design of computer circuits;
- 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 integrated 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;
- Logic programming;
- Definition of formal languages;
- 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.
Read more about Logic In Computer Science: Books
Famous quotes containing the words logic in, logic, computer and/or science:
““... We need the interruption of the night
To ease attention off when overtight,
To break our logic in too long a flight,
And ask us if our premises are right.””
—Robert Frost (1874–1963)
“Somebody who should have been born
is gone.
Yes, woman, such logic will lead
to loss without death. Or say what you meant,
you coward . . . this baby that I bleed.”
—Anne Sexton (1928–1974)
“Family life is not a computer program that runs on its own; it needs continual input from everyone.”
—Neil Kurshan (20th century)
“It is clear that everybody interested in science must be interested in world 3 objects. A physical scientist, to start with, may be interested mainly in world 1 objects—say crystals and X-rays. But very soon he must realize how much depends on our interpretation of the facts, that is, on our theories, and so on world 3 objects. Similarly, a historian of science, or a philosopher interested in science must be largely a student of world 3 objects.”
—Karl Popper (1902–1994)