2A SE

SE212: Logic and Computation

This course builds on top of MATH135. It’s 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: