This course builds on top of MATH135

SE212: Logic and Computation §

This course is about Logic and sets, and their use in software engineering and computer science. We study the use of logic for:

• Specifying the behaviour of systems
• Checking the correctness of programs

https://student.cs.uwaterloo.ca/~se212/

The 4 major topics of the course:

• Propositional Logic
• Predicate Logic
• Set Theory and Formal Specification
• Program Correctness using Floyd-Hoare Logic

Link to course notes here.

• Specification = describing what the software is supposed to do, see Formal Specification
• Correctness = the software does what it is supposed to do, see Program Correctness
  • We check correctness in 3 ways.
  1. Inspection
  2. Testing Blackbox Testing and Whitebox Testing
  3. Formal Verification $\to$ What we learn SE212

Concepts §

• Syllogism
• Formal Verification
• george
• Module 2: Propositional Logic
  • Boolean Valuation
  • Tautology
  • Logic: Relating Semantics to Proof Theory
  • Soundness
  • Completeness
  • Contradiction
  • Contingent Formula
  • Normal Form
  • Logical Implication
  • Logical Equivalence
  • Transformational Proof
  • Normal Form
  • Goals vs. Theorems
  • Subcategories of Proof Theory:
    • Transformational Proof (TP)
    • Natural Deduction (ND)
      • Inference Rule
      • Subproof
    • Semantic Tableaux (ST)
• Module 3: Predicate Logic
  • Free Variable
  • Type Inference
• Module 4: Theory
  • Enthymeme
  • Leibniz’s Law
  • Gödel’s Incompleteness Theorems
  • Satisfiable Modulo Theories Solver
• Module 5: Set Theory
  • Z Notation
  • Binary Relation
• Module 6: Formal Specification in Z
  • Z Specification
  • Schema
• Module 7: Program Correctness
  • Floyd-Hoare Logic
  • Vacuous Truth
  • Termination
  • Variable Capture
  • Partial Correctness
  • Total Correctness
  • Function value proofs
  • Halting Problem
  • Bounding Function

Related §

• These are concepts that are not covered, but that the professor mentioned
  • Temporal Logic
• Spatial Temporal Reasoning

As I was studying for my final exam, I started thinking about Semantics and Artificial Intelligence

• Well, there are strides in NLP, the AI manages to learn about these ideas in some sort of Latent Space

Precedence for this course: