Диссертация (Автоматический логический вывод в интуиционистских логических исчислениях обратным методом Маслова), страница 5

Н. Колмогоров предложил интерпретацию интуиционистской логики каклогики задач, которая впоследствии получила название интерпретации Брауэра —Гейтинга — Колмогорова(BHK).ПозднееС. К. Клинипредложилинтерпретацию в терминах рекурсивной реализуемости (см.

подробное изложениеэтой концепции в книге [13]).Немного другим путем пошли представители конструктивного направленияв математике, развиваемого научной школой А. А. Маркова. В отличие отинтуиционистов, конструктивисты для обоснования математических построенийиспользуют точное понятие алгоритма. Преимущество алгоритмов заключается втом, что они сами являются конструктивными объектами, поэтому их можно22исследовать математическими методами.

Подробнее конструктивная математикаобсуждается в трудах А. А. Маркова [19] и Н. А. Шанина [51].Согласно А. Г. Драгалину [9, с. 508], конструктивное направление вматематике можно рассматривать как разновидность интуиционизма в широкомсмысле. Сегодня различие между терминами «интуиционистская логика» и«конструктивная логика» практически стерлось: эти термины понимаютсядостаточно широко и могут использоваться для обозначения различныхвариантов интуиционистской (конструктивной) логики.

В настоящей работе этитермины рассматриваются как синонимы, равно как термины «интуиционистскоеисчисление» и «конструктивное исчисление».Конструктивный характер интуиционистской логики впоследствии оказалсяполезен и в информатике. Х. Карри, У. Ховард и ряд других ученых в 1968–1969 годах исследовали связь исчислений типов с импликативной логикой, азатем и с интуиционистским исчислением предикатов (см. [88]).

Идея построениятакого соответствия и ее варианты в литературе могут «скрываться» под разныминазваниями: «типы как доказательства», «высказывания как типы», «изоморфизмКарри — Ховарда», «доказательства как программы»19. Термин «доказательствакак программы» был предложен в статье [55], где была рассмотрена возможностьиспользовать(интуиционистскую)логикувкачествебазыдляязыкапрограммирования. Этот подход был реализован в интерактивной программеАЛВ Nuprl, а затем и в других интерактивных программах АЛВ, которыеподробнее обсуждаются в следующем параграфе. Согласно Р.

Л. Констеблю [65],корни самой идеи можно проследить еще в интерпретациях А. Н. Колмогорова иС. К. Клини.Подробное изложение идей интуиционизма, а также обсуждение раннихработ по интуиционистской логике можно найти в книгах А. Гейтинга [4],С. К. Клини и Р. Ю. Весли [15], в сборнике А. С.

Трулстра [150], в сборникетрудов А. Г. Драгалина [9], а также в более современной статье А. С. Трулстра19В англоязычных источниках используются термины «proofs-as-types», «formulas-as-types», «propositions-as-types», «Curry — Howard correspondence» и «proofs-as-programs».23[148]. Русскоязычный перевод книги А. Гейтинга [4] также интересен тем, чтосодержиткомментарииА. А. Маркова,проясняющиеразличиямеждуинтуиционизмом Брауэра и конструктивным подходом.1.4. Программы автоматического логического вывода и области ихпримененияПрограммы автоматического логического вывода можно условно разделитьна два основных типа: интерактивные и автоматические «пруверы»20.

Винтерактивных «пруверах», как правило, используются логики высших порядковили теории типов. В таких программах полуавтоматический процесс поискадоказательств управляется пользователем. Автоматические «пруверы», какправило, предназначены для менее выразительных логик: для логики первогопорядка (с равенством) или для логики высказываний. Однако при этом такиепрограммы способны выполнять поиск доказательств в автономном режиме.В этом параграфе изложен краткий обзор существующих программ АЛВ иобластей их применения.

Больше информации можно найти в следующихисточниках: [135, 82, 90]. Эти статьи, в частности, использовались присоставлении обзора, приведенного в настоящем параграфе. Для читателей,которые заинтересуются применением интерактивных программ АЛВ, такжемогут оказаться полезными публикации [160, 161], где приведено сравнение такихпрограмм по различным критериям.1.4.1. Применение программ автоматического логического выводаВ настоящее время программы АЛВ успешно применяются для решенияряда актуальных задач, как научных, так и практических.

Области применениятаких программ не ограничиваются математикой и включают верификациюразличных программных и аппаратных систем, логический вывод в системах20Ванглоязычнойлитературеинтерактивные«пруверы»автоматические — «automated theorem provers» или просто «provers».называются«proofassistants»,а24искусственного интеллекта и т.

д. Вопросы автоматизации доказательствизучаются учеными в крупнейших исследовательских институтах мира.В математике программы АЛВ используются как «умные помощники» дляпроведения рутинных доказательств или сведения сложных теорем к болеепростым промежуточным леммам. Примером успешного применения программАЛВ в математике является доказательство гипотезы Г. Роббинса, котороеполучил У. МакКьюн с помощью программы EQP (одна из версий программыOtter) [105].

На основе этого машинного доказательства было полученотрадиционное математическое доказательство гипотезы Роббинса.Бурное развитие интерактивных «пруверов» привело к появлению новогометода доказательства математических теорем — компьютерной формализации.Теорема считается формализованной, если найдено ее доказательство в рамкахкакой-либо непротиворечивой формальной аксиоматической теории (например, висчислении предикатов) и это доказательство прошло процедуру верификации(проверки). Как правило, для сложных теорем полная формализация возможнатолькоспомощьюкомпьютера.Например,следующиематематическиеутверждения были формализованы компьютерными методами: теорема о четырех красках, в программе Coq [77]; теорема о распределении простых чисел, в программе Isabelle [52]; теорема Жордана о кривой в пространстве, в программах HOL Light [80] иMizar [94]; задача со счастливым концом для случая 17 точек [138]; теорема Фейта — Томпсона, в программе Coq [76].Список успешно формализованных теорем регулярно пополняется.

Какправило, машинные доказательства ввиду своего объема не могут быть проверенывручную. Однако за счет полной машинной верификации при соблюдении такназываемогопринципадеБрейна[54]вероятностьошибкивтакихдоказательствах может быть значительно ниже, чем в объемных доказательствах,полученных вручную.25Наиболее востребованной промышленной областью применения программАЛВ на сегодняшний день остается верификация (формальная проверка)аппаратного обеспечения. Например, для формальной верификации процессорови других устройств Intel, AMD, Rockwell Collins и IBM использовалисьпрограммы HOL Light [83], ACL2 [61, 93] и PVS [133].Задача верификации ПО является еще более трудной, однако и в этомнаправлении уже достигнуты положительные результаты.

Экспериментальнаяпрограмма Karlsruhe Interactive Verifier (KIV) была успешно использована напрактике для верификации ряда компьютерных программ, в частности, дляпроверки компилятора языка Пролог [125]. При помощи программы PVSпроверялись алгоритмы диагностики и планирования для отказоустойчивыхархитектур [113]. Одна из модификаций программы RRL применялась дляверификации ряда простых программ [91].Области применения программ АЛВ также включают верификацию сетевыхпротоколов [158, 81], синтез программного обеспечения [131, 159], системыкомпьютерного зрения [59], семантические сети, онтологии [151, 87] и другиеприложения искусственного интеллекта[92, 74, 146].

Другие примерыприменения программ АЛВ на практике можно найти в статьях [135, 82].1.4.2. Роль интуиционистских теорий в современных программах АЛВВ интерактивных «пруверах», таких как Coq [142], Agda [60, 141] и Nuprl[119], важную роль играют интуиционистские (конструктивные) теории. Какправило, в подобных программах используются различные модификации теориитипов Мартин-Лефа [103]. Предложенный в статье [55] подход «доказательствакак программы» позволяет встроить в программу АЛВ полноценный языкпрограммирования, внутри которого «спрятана» интуиционистская теория типов.Условно говоря, такой язык позволяет описать формальную спецификациюпрограммы. Формулу, соответствующую этой спецификации, требуется доказатьв нижележащей теории типов.

Если это не удается сделать, программа не26компилируется. Если же доказательство найдено, то из него извлекаетсяпрограмма в функциональном стиле. Поэтому авторы утверждают, что ихинтерактивные «пруверы» позволяют создавать программы, корректные попостроению («correct by construction»). Видимо, данное утверждение следуетпонимать в предположении о корректности ядра интерактивного «прувера», вкотором реализованы основные алгоритмы поиска вывода и извлечения программиз доказательств.

Как правило, разработчики стараются делать это ядро какможно более компактным [78], но это не дает 100 % гарантии отсутствия ошибок.В статье [65] приведены примеры использования конструктивных теорийтипов, реализованных в Coq и Nuprl, для формальной верификации ПО [97],операционных систем [130] и распределенных систем [120, 126].В программах Coq и Nuprl реализован механизм тактик, который позволяетрешать достаточно сложные задачи, такие как верификация ПО.

В число этихтактик входят автоматизированные тактики для интуиционистской логикипервого порядка. Например, автоматический «прувер» JProver [127] встроен вCoq, Nuprl и MetaPRL. Однако имеющиеся интуиционистские тактики трудноназвать очень эффективными. В качестве подтверждения можно привестирезультаты программы JProver на задачах из библиотеки ILTP [144], а такжерезультатысравненияизстатьи[96].Внедрениеболеемощныхавтоматизированных тактик позволило бы в ряде случаев сократить объем ручнойработы для пользователей интерактивных «пруверов», так как существуютфрагменты интуиционистских теорий типов, для которых задачу поиска выводаформулможнонапрямуюсвестикзадачепоискавыводаформулвинтуиционистской логике первого порядка [139].Рассмотрим подробнее существующие автоматические «пруверы» дляинтуиционистской логики первого порядка, чтобы понять причины текущегоположения дел.

В таблице 1.1 приведены сведения о наиболее известныхинтуиционистских программах АЛВ. Для каждой программы указано ее название,язык программирования, на котором она реализована, используемый методлогического вывода (методы логического вывода подробнее обсуждаются в27следующем параграфе) и при наличии адрес сайта.

В таблице «звездочкой»помечены программы, результаты тестирования которых приведены на сайтеILTP [144].Таблица 1.1. Программы АЛВ для интуиционистской логикиПрограммаЯзыкреализацииМетод доказательстваСайт21––ft-C*ft-Prolog*GandalfCPrologSchemeМетод аналитических таблицМетод аналитических таблицОбратный метод Масловаhttp://deepthought.ttu.ee/it/gandalf/JProver*OCamlТабличный метод («non-clausalconnection calculus»)https://github.com/coqcontribs/jprover/,http://metaprl.org/install.htmlileanCoP*PrologileanTaP*PrologileanSeP*PrologImogenStandard ML,Haskell, ScalaОбратный метод Масловаhttps://github.com/seanmcl/imogennanoCoP-iPrologТабличный метод («non-clausalconnection calculus»)http://www.leancop.de/nanocopi/index.htmlТабличный метод («clausalconnection calculus»)Метод семантических таблицМодификация методааналитических таблицhttp://www.leancop.de/ileancop/http://www.leancop.de/ileantap/http://www.leancop.de/ileansep/Программы ft-C и ft-Prolog не имеют своего сайта и представляют собойреализации одного и того же логического исчисления [124] на разных языкахпрограммирования — C и Prolog соответственно.Программа JProver может использоваться либо как самостоятельнаяпрограмма АЛВ, либо как часть систем MetaPRL, Coq или Nuprl.

Описаниепрограммы JProver приводится в статье [127].Программа ileanCoP создана Дж. Оттеном на основе программы leanCoP дляклассической логики. Программы ileanTaP, ileanSeP и nanoCoP-i написаны тем жеавтором, но отличаются используемыми логическими исчислениями.ПрограммаGandalfдляинтуиционистскойлогикибыласозданаТ.