TouIST in Progress

This work deals with logical formalization and problem solving using automated solvers.The goal of TO UIST is to allow the user to concentrate on the modeling of a given problem without worrying about the technical details related to the use of solvers: TO UIST provides a simple language to generate logical formulas (as an input to solvers) from a problem description, and allows to model many static or dynamic combinatorial problems.All this can be very helpful as a teaching support for logics and discrete mathematics.Users may benefit from the regular improvements of SAT, QBF, or SMT solvers to solve concrete problems efficiently, e.g., different classes of planning tasks in Artificial Intelligence.We consider recent updates to TO UIST dealing with modal logic (mostly due to the first author), and discuss possible applications of TO UIST in scientific research.