Logic in computer science

https://en.wikipedia.org/wiki/Logic_in_computer_science https://en.wikipedia.org/wiki/Category:Logic_in_computer_science

Logic in computer science covers the overlap between the field of logic and that of CS. The topic can essentially be divided into 3 main areas:

• Theoretical foundations and analysis

• Use of computer technology to aid logicians

• Use of concepts from logic for computer applications

Logic in CS, or computational logic, is a field on the intersection between mathematical logic and computer science containing:

• investigations into logic that are guided by applications in CS:

  • Rewriting systems

  • Combinatory logic

  • Abstract interpretation

• Fundamental concepts in CS that are naturally expressible in logical form:

  • Type theory

  • Formal semantics of programming languages

  • Hoare logic

  • Logic programming

• Applications of fundamental concepts derived from the theory of computation:

  • Curry-Howard correspondence

  • Game semantics

• Tools for logicians considered as applied CS:

  • Automated theorem proving

  • Model checking