David Stanovskı    //   

MATHEMATICAL SOFTWARE 2017/18

Program:

Weeks 1-7: David Stanovskı on computational logic tools
Weeks 8-14: Faruk Göloglu on Sage and cryptography

Computational logic:

  • Boolean satisfaction, SAT-solving
  • Satisfaction modulo theories
  • Automated thorem proving in first order logic
Preparation for the second part (Deadline: mid November):
Learn basics of Python!!!
covered topicsrecommended reading homework
5.10.Boolean satisfaction. Translating problems to SAT. Knights and Knaves
12.10.Translating problems to SAT, SAT-solving in practice. viz resources about SAT below
19.10.Principles of SAT-solving, clausification. viz resources about SAT below HOMEWORK due on 2.11.
26.10.Principles of SMT-solving. Oliveras's slides
2.11.SMT-solving in practice. Translating problems to SMT. Z3 tutorial
9.11.Lecture will probably be cancelled, come to the fall school of algebra! (Or, learn Python!)
16.11.Automated theorem proving in first order logic. HOMEWORK due on 11.1.
23.11.??? Princples of CSP solving, Minizinc. ???


Resources about SAT: Resources about SMT: Resources about First order ATP: Resources about First order ATP: