JetBrains Research — наука, меняющая мир

Семинар по автоматизации доказательств при помощи Coq Hammer

Системы интерактивного доказательства теорем становятся все более важным инструментом в процессе сертификации математических доказательств и свойств программного обеспечения. Значительная часть процесса формализации состоит из утомительного доказательства небольших тривиальных утвеждений. Техники автоматизации поиска доказательства способны существенно упростить этот процесс. "Hammer" (молоток) --- это утилита автоматизации поиска доказательств общего назначения, которая позволят транслировать проблему из логики ITP системы в менее выразительный язык логики первого порядка и попробовать решить ее при помощи систем автоматического доказательста теорем (SAT/SMT provers).

В данном докладе будет представлен обзор "Hammer" утилиты для системы интерактивных доказательств Coq.

Материалы к докладу:

Czajka, Ł., & Kaliszyk, C. (2018). Hammer for Coq: Automation for dependent type theory. Journal of automated reasoning, 61 (1-4), 423-453.

Докладчик --- Евгений Моисеенко

22.04.2019, 17:15.

Место: ауд. 3248, мат-мех. факультет СПбГУ, Старый Петергоф, Университетский пр-т, д. 28