Overview
A set of Isabelle proof methods and commands that facilitates the use of relatively complete decision procedures (e.g. SMT solvers and paramodulation-based provers) with deterministic quantifier instantiation based on bounded E-matching. More about TSMT is explained in the TSMT Tutorial.
Issue tracking Details
Members
Manager: Alexey Khoroshilov, Mikhail Mandrykin
Developer: Alexey Demakov, Alexey Khoroshilov, Denis Buzdalov, Grigoriy Volkov, Mikhail Mandrykin, Pavel Ivanov, Александр Крюков, Рафаэль Садыков
Project Creator: Alexey Khoroshilov, Mikhail Mandrykin