Цель курса – сформировать представление о теоретической и практической значимости решения задачи SMT, и об основных методах решения данной задачи. Дать представление о применимости автоматизированного доказательства теорем в различных областях математики и информатики, особенно в сфере формальной верификации программ. Познакомить со способами реализации методов решения задачи SMT в программных системах для автоматизированной проверки выполнимости формул в теориях первого порядка.