Natural Deduction

Prooftree

Sequent Calculus

Direct proof

Modal Logic

Proofs as Programs

Logic Programming

Kolmogorov translation

Heyting Arithmetic

Induction

Prolog in Prolog

Prolog

Backward Chaining

Refutation Proofs

Admissibility

Ordered Proofs as Concurrent Programs

Focusing

Verifications

Subsingleton Logic

Quantification

Functional Logic

Fitch Proofs

Cut Elimination

Verifications and Uses

Depth estimation

Propositional Theorem Proving

Classical Logic

Derivability

Session Types

Relational Logic

Harmony

Linear logic applications

Equality

Ordered Logic

Linear Logic

Inversion

Proofs as ML programs

Propositional Analysis

Propositional calculus (Propositional logic)

Monads

Practical Prolog

Forward Chaining

Lax logic 

Certifying Theorem Provers

Relational Analysis

CS 157 Introduction to Logic Stanford University Fall 2022 CS 157 provides a rigorous introduction to Logic from a computational viewpoint. The course mainly deals with encoding information as logical sentences and reasoning methods for this information. It gives an overview of logic technology and its applications. Topics range from propositional logic, relational logic, functional logic to various deduction techniques and mathematical induction. CS 157 is a rigorous introduction to Logic from a computational perspective. It focusses on the encoding of information in the form of logical sentences; it covers various methods for reasoning with information in this form; and it provides an overview of logic technology and its applications (in mathematics, science, engineering, business, law, and so forth). Topics include the syntax and semantics of Propositional Logic, Relational Logic, and Functional Logic, validity, contingency, unsatisfiability, logical equivalence, entailment, consistency, direct deduction (Hilbert), natural deduction (Fitch), refutation reasoning (Resolution), mathematical induction, compactness, soundness, completeness.   

CS 157 Introduction to Logic

15-317 / 15-657 Constructive Logic Carnegie Mellon University Fall 2021 This undergraduate course introduces students to constructive logics such as intuitionistic and linear logic, focusing on their use in computer science. The goal is to understand the distinction between classical and constructive logic, define logical connectives, implement theorem provers, and explore computational interpretations of logics. Concepts covered include natural deduction, sequent calculus, logic programming, linear logic, and many more. This undergraduate course provides an introduction to constructive logics, such as intuitionistic and linear logic, with an emphasis on their application in computer science. This includes basic means for defining logics (for example, natural deduction and sequent calculus), establishing properties of logics (for example, cut elimination), and for investigating their computational interpretations (for example, via proof reduction or proof search). After taking this course, students should be able to

- understand the distinction between classical and constructive logic, and the uses of constructive logic
- define logical connectives and test these definitions for harmony
- express and prove the relationships between different representations of a logic (e.g., natural deduction and sequent calculus), and explain what each representation is for
- implement propositional theorem provers
- use operational interpretations of logics via proof search (a.k.a. logic programming)
- understand the applications of substructural logics  

15-317 / 15-657 Constructive Logic

Logic in Computer Science is the application of formal logic to the field of computing. Formal logic provides a systematic framework to represent and reason about propositions, predicates, and arguments. Logic in Computer Science typically involves Boolean logic, propositional logic, predicate logic, and sometimes more advanced topics such as temporal logic and modal logic.

The field includes the study of various logic-based languages, the use of logic in formal methods for software and hardware verification, the application of logic in AI and databases, and more.

Logic

Computer Science

Logic

Prerequisites

Common concepts