Coq 8.12.1 (доказательство теорем)

Опубликовано August@Karro - чт, 11/19/2020 - 02:21
Coq — интерактивное программное средство доказательства теорем, использующее собственный язык функционального программирования (Gallina) с зависимыми типами.

Теоретической базой Coq считается исчисление конструкций; в названии скрыта его аббревиатура (CoC, англ. calculus of constructions) и сокращение от фамилии создателя исчисления — Тьерри Кокана. Позволяет записывать математические теоремы и их доказательства, удобно модифицировать их, проверяет их на правильность. Пользователь интерактивно создаёт доказательство сверху вниз, начиная с цели (то есть от гипотезы, которую необходимо доказать).

Coq может автоматически находить доказательства в некоторых ограниченных теориях с помощью так называемых тактик. Coq применяется для верификации программ. В новой версии была значительно доработана стандартная библиотека и документация, а также исправлен ряд ошибок.

Тактика автоматически генерирует доказательство (или его часть), опираясь на цель (что нужно доказать). Конечно, чтобы тактика сработала, должен существовать алгоритм поиска доказательства. В некоторых случаях тактики могут сильно уменьшить объём доказательства.

Чтобы использовать тактики, необходимо после Definition указать тип (цель, высказывание, которое нужно доказать), но опустить лямбда-терм, то есть само доказательство. Тогда Coq переходит в режим редактирования доказательства, где можно построить доказательство с помощью тактик. 


Coq разработан во Франции в рамках проекта TypiCal (ранее — LogiCal), совместно управляемом INRIA, Политехнической школой, Университетом Париж-юг XI и Национальным центром научных исследований, ранее была выделенная группа и в Высшей нормальной школе Лиона. 

 

Последние материалы