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/<https://emea01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fsmtlib.cs.uiowa.edu%2F&data=01%7C01%7Cdaniele.magazzeni%40kcl.ac.uk%7C885af824259e4601730f08d48b0fd296%7C8370cf1416f34c16b83c724071654356%7C0&sdata=Hi%2B18fTp%2FDjlAbw2QENyHVj8hjyVtCReClWN3N89Jzw%3D&reserved=0> - PySMT (www.pysmt.org<https://emea01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.pysmt.org&data=01%7C01%7Cdaniele.magazzeni%40kcl.ac.uk%7C885af824259e4601730f08d48b0fd296%7C8370cf1416f34c16b83c724071654356%7C0&sdata=NnrJitTKF1SxHSPqMN8YDEeL%2BXRB4anxLPq6rK%2BHQRM%3D&reserved=0>) -> check out the example directory in the repo and the documentation at https://pysmt.readthedocs.io/en/latest/<https://emea01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fpysmt.readthedocs.io%2Fen%2Flatest%2F&data=01%7C01%7Cdaniele.magazzeni%40kcl.ac.uk%7C885af824259e4601730f08d48b0fd296%7C8370cf1416f34c16b83c724071654356%7C0&sdata=UzgkYy9g5zqPx8nRHCw1Ht%2FyvcahP2oxHep7K7phmXI%3D&reserved=0> - Roberto Sebastiani's course on SAT/SMT at UniTN: http://disi.unitn.it/~rseba/DIDATTICA/SAT_BASED16/<https://emea01.safelinks.protection.outlook.com/?url=http:%2F%2Fdisi.unitn.it%2F~rseba%2FDIDATTICA%2FSAT_BASED16%2F&data=01%7C01%7Cdaniele.magazzeni%40kcl.ac.uk%7C885af824259e4601730f08d48b0fd296%7C8370cf1416f34c16b83c724071654356%7C0&sdata=TNumoJzY1bobNcLVfOvZX062xaEwSrPglqluKjrtXRU%3D&reserved=0> Please do not hesitate to contact me for other SMT-related questions and remarks. Regards, Andrea Micheli