Automated Reasoning

We shall introduce the main technologies employed in automated reasoning, based both on saturation and on backtracking methods. Applications covering computational algebra topics as well as formal verification problems will be considered. The student will be introduced to some state-of-the-art tools, like SAT- and SMT-solvers, superposition provers, finite and infinite state model checkers.

To be acquainted with automated reasoning tools (SMT-solvers and superposition provers), from the point of view both of practical use and of theoretical foundations.