Войти / Регистрация
Корзина

  • Ваша корзина пуста
Войти / Регистрация
Корзина

  • Ваша корзина пуста

Статья «СИСТЕМА АВТОМАТИЧЕСКОГО ДОКАЗАТЕЛЬСТВА ТЕОРЕМ ИНТУИЦИОНИСТСКОЙ ЛОГИКИ НА ОСНОВЕ ОБРАТНОГО МЕТОДА, "Программирование"»

Авторы:
  • Павлов В.А.1
  • Пак В.Г.2
стр. 46-59
Платно
1 ГБОУ ВПО «Тихоокеанский государственный медицинский университет» Минздрава России, 2 Санкт-Петербургский политехнический университет Петра Великого
  • В выпуске: №1, 2018
  • В журнале: Программирование
  • Издательство: ФГУП «Издательство «Наука»
  • Рубрика ГРНТИ: Информатика. Информационные и вычислительные системы
  • Год выхода: 2018
  • SDI: 007.001.0132-3474.2018.000.001.4
  • УДК: 004.832.32
Аннотация:
Интуиционистская логика первого порядка - это одна из формальных теорий семейства конструктивных логик. В интуиционистской логике можно получить экземпляр элемента x = а наряду с доказательством формулы P(а) из вывода формулы 3xP(x). Благодаря этой возможности интуиционистская логика находит многочисленные применения в математике и информатике. Многие современные пруверы (программы автоматического доказательства теорем) имеют встроенные реализации алгоритмов оптимизации поиска доказательств в логиках первого порядка, упрощающие решение сложных проблем, таких как формальная верификация программного обеспечения, микросхем или протоколов. В настоящей статье представлен новый прувер (названный нами WhaleProver) для полной интуиционистской логики первого порядка. Тестирование на задачах библиотеки ILTP показало, что возможности WhaleProver сравнимы с лучшими современными аналогами. Наша программа решила более 800 задач библиотеки ILTP (версия 1.1.2), некоторые из которых не разрешимы для других пруверов. Программа WhaleProver основывается на обратном методе, предложенном С.Ю. Масловым. В статье представлено интуиционистское исчисление для обратного метода, являющееся, в свою очередь, секвенциальным исчислением специального вида. Также описаны адаптации некоторых известных стратегий оптимизации поиска доказательств для этого исчисления, которые были разработаны для различных исчислений С.Ю. Масловым, В.П. Оревковым, А.А. Воронковым и другими авторами. Дополнительно предложена новая стратегия, позволяющая избежать порождение избыточных выводов. В статью включены результаты экспериментов нашего прувера с задачами из библиотеки ILTP. Мы уверены, что он может в перспективе использоваться как для тестирования различных алгоритмов доказательства и стратегий оптимизации, так и для образовательных целей.

Архивные статьи (2015 год и ранее) доступны для ознакомления бесплатно, для скачивания их необходимо приобрести. Для просмотра материалов необходимо зарегистрироваться и авторизоваться на сайте.

Чтобы приобрести доступ к материалу для юридического лица, пожалуйста, свяжитесь с администрацией портала с помощью формы обратной связи либо по электронному адресу libnauka@naukaran.com.  

Действия с материалами доступны только авторизованным пользователям.