Computer Assisted Proofs

M1 IF course, ENS de Lyon. Friday 10:15 - 12:15, Amphi B.

Contents

  1. Foundations of interactive theorem proving
    • The Coq System
    • Curry-Howard Correspondance:
      • Propositional Logic
      • Arithmetic
      • Polymorphism
  2. Foundations of automatic theorem proving
    • Sequent calculus
    • Herbrand's theorem
    • The resolution method

Useful stuff

Courses

















Valid XHTML 1.0 Strict



Back home.