Date: 2013-11-13
Categories: news; teaching

PhD student course on logic, proof and mechanized theorem proving

On Wed 2013-11-13 and Wed 2013-11-20 I am giving a course on logic, proof and theorem proving to current PhD students. The following is my rough plan for the two sessions (each 1 hour long). Students are expected to read material beforehand.

Reading:

  * basic background

    http://www.paultaylor.eu/stable/prot.pdf
    Ch.s 1-5 (4 is slightly less important for theorem proving)

    http://en.wikipedia.org/wiki/Logical_connective

    http://en.wikipedia.org/wiki/Natural_deduction

    http://en.wikipedia.org/wiki/Sequent_calculus


  * intro to proof theory:

    http://plato.stanford.edu/entries/proof-theory-development/


  * the system LJ:

    http://www.normalesup.org/~saurin/Enseignement/Proof_Theory_CMI/cours3.pdf

Session 1:

1st session
===========

  Connectives

  Propositional logic

  Meaning of propositional statements, truth tables

  Propositional proofs 

    Two types of proof: ND, sequent calculus

  Quantifiers

  Meaning of statements involving quantifiers, models

  First-order proofs (ND, sequent calculus)

  System G3i

  The cut rule

  Proof and types  

Session 2:

2nd session
===========

  Introduction to HOL

  Basic steps with HOL

  Simple proofs

  First-order automated proof

  Simplification  

  Induction


Related articles:

  • 2017-09-06 ICFP most influential paper from 10 years ago
  • 2017-03-16 tjr-btree: a CoW B-tree library in OCaml
  • 2016-06-05 Do not buy TP-Link products
  • 2016-05-27 Visit to Cambridge, for REMS workshop
  • 2016-04-22 Visit to Denmark, to see Joergen Villadsen
  • 2016-02-19 Tree-structured text
  • 2016-02-09 Simple implementation of an Earley-like parsing algorithm
  • 2016-01-27 Talk at York University
  • 2016-01-06 Stephanie Heintz PhD viva
  • 2015-10-05 SibylFS presentation at SOSP'15
  • 2015-09-28 SibylFS SOSP poster
  • 2015-09-21 SibylFS presentation to Industrial Advisory Board
  • 2015-06-28 SOSP 2015 paper acceptance for SibylFS
  • 2015-04-21 REMS Cambridge talk on SibylFS
  • 2014-11-21 Talk on parsing at the University of Sussex
  • 2014-09-26 P1 combinator parsing library for OCaml
  • 2014-09-26 E3 earley parser library for OCaml
  • 2014-09-18 SLE 2014 conference, and Parsing at SLE workshop, slides
  • 2014-09-07 ICFP 2014, OCaml workshop, slides and video
  • 2014-09-07 ICFP 2014, Lem talk
  • 2014-07-11 P3 paper accepted for SLE 2014
  • 2014-07-11 Lem paper accepted to ICFP 2014
  • 2014-04-15 New release of P3 code on github
  • 2014-03-02 New release of P3 code on github
  • 2013-12-16 New release of P3 code on github
  • 2013-12-03 Implementing algorithms efficiently
  • 2013-11-24 Experience of using Lem
  • 2013-11-13 PhD student course on logic, proof and mechanized theorem proving
  • 2013-11-13 New website design
  • 2013-11-13 Engineer position
  • 2013-11-12 Netsem TCP/IP specification on github
  • 2013-11-08 Talk on parsing and P3 given at Cambridge
  • 2013-11-01 Funded PhD positions
  • 2013-04-01 PhD position funded by Microsoft Research
  • 2013-02-01 EPSRC grant funded