# Logic

There have been 1 completed talk and 6 topic suggestions tagged with **logic**.

## Related Tags

- computability
- constructive mathematics
- theoretical computer science
- set theory
- computer science
- turing machine
- real analysis
- incompleteness

## Completed Talks

### Constructive analysis

Delivered by Fengyang Wang on Wednesday November 1, 2017

Constructive mathematics, as the name would suggest, is centered on the philosophy that mathematical proofs should be able to be turned into algorithms. We will contextualize constructive approaches to analysis, roughly following Bridges and Vîţă. This talk has no formal prerequisites beyond an elementary understanding of the real numbers and the usual concept of completeness. In particular, no logical background is assumed; intuitionistic logic will be overviewed in the talk. We will finish with a discussion of the ramifications of completeness of the real numbers.

A summary of this talk is available here.

## Talk Suggestions

### Automated Verification of Computational Systems

It was realized in the 1960s that mathematical logic provides a suitable language to formulate properties of programs. This idea was formalized by Hoare who developed *Hoare logic* as a means to prove program correctness. However, this technique didn't apply directly to concurrent programs. An alternative approach called *Temporal Logic* was proposed by Amir Pneuli in 1977 which did provide a means to reason about concurrent programs. This topic studies this and then delves into the fundamental ideas behind model checking.

**Required Background:** Basics of computer science at the level of CS 146, Logic at the level of CS 245.

Possible reference materials for this topic include

Grumberg, O., & Veith, H. (Eds.). (2008). 25 years of model checking: history, achievements, perspectives (Vol. 5000). Springer.

Quick links: Google search, arXiv.org search, propose to present a talk

computer science logic model checking

### Completeness, Incompleteness, and Turing Machines

This topic studies the connection between Gödel’s incompleteness theorems and turing machines and how each implies the other

Possible reference materials for this topic include

Quick links: Google search, arXiv.org search, propose to present a talk

computability computer science incompleteness logic theoretical computer science turing machine

### Constructive Mathematics

Constructive mathematics, or mathematics without the law of the excluded middle, is becoming more popular thanks to connections with computer science, category theory, and topology. Its logical foundations may be initially difficult to grasp for those used to a classical system.

Possible reference materials for this topic include

Quick links: Google search, arXiv.org search, propose to present a talk

computability computer science constructive mathematics logic philosophy topology type theory

### Curry–Howard–Lambek Correspondence

Possible reference materials for this topic include

Quick links: Google search, arXiv.org search, propose to present a talk

category theory computer science logic

### Lindenmeyer systems

Originally developed to model plant growth, L-systems are a logical approach to various scientific questions, as well as one of many ways to generate artistically pleasing fractals.

Possible reference materials for this topic include

Quick links: Google search, arXiv.org search, propose to present a talk

art biology botany computability computer science fractal logic theoretical computer science

### Presburger Arithmetic

Possible reference materials for this topic include

Quick links: Google search, arXiv.org search, propose to present a talk

computability computational complexity computer science logic theoretical computer science