> For the complete documentation index, see [llms.txt](https://mandober.gitbook.io/math-debrief/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://mandober.gitbook.io/math-debrief/300-logic/terms/logic-in-cs.md).

# 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
