Hi all,

Please find below an email from Andrea with material on SMT.

Many thanks Andrea!

Best

Dan

--

Dr Daniele Magazzeni

Lecturer in Artificial Intelligence, King's College London

Head, AI Planning Group

Editor-in-Chief, AI Communications

http://www.inf.kcl.ac.uk/staff/danmag

Hi all,

in attach you can find the slides presented during Friday's class on SMT together with some additional slides I had on PySMT and the Quantifier Elimination Algorithm for Linear Integer Arithemtic (Cooper's Method).

In addition, you can find additional material on SMT at the following links:

- SMT-LIB initialtive: http://smtlib.cs.uiowa.edu/

- PySMT (www.pysmt.org) -> check out the example directory in the repo and the documentation at https://pysmt.readthedocs.io/en/latest/

- Roberto Sebastiani's course on SAT/SMT at UniTN: http://disi.unitn.it/~rseba/DIDATTICA/SAT_BASED16/

Please do not hesitate to contact me for other SMT-related questions and remarks.

Regards,

Andrea Micheli