Научно-технические ведомости Санкт-Петербургского политехнического университета. Информатика. Телекоммуникации. Управление
RUS  ENG    ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ПАКЕТ AMSBIB  
Общая информация
Последний выпуск
Архив

Поиск публикаций
Поиск ссылок

RSS
Последний выпуск
Текущие выпуски
Архивные выпуски
Что такое RSS


Информатика, телекоммуникации и управление:
Год:
Том:
Выпуск:
Страница:
Найти




Персональный вход:
Логин:
Пароль:
Запомнить пароль
Войти
Забыли пароль?
Регистрация

Научно-технические ведомости Санкт-Петербургского политехнического университета. Информатика. Телекоммуникации. Управление, 2015, выпуск 6(234), страницы 70–80
DOI: https://doi.org/10.5862/JCSTCS.234.7 (Mi ntitu137) 		 
Интеллектуальные системы и технологии

Экспериментальная программа для доказательства теорем интуиционистской логики обратным методом Маслова

В. А. Павлов, B. Г. Пак

Институт компьютерных наук и технологий Санкт-Петербургского политехнического университета Петра Великого
PDF полного текста (344 kB)
DOI: https://doi.org/10.5862/JCSTCS.234.7
Аннотация: Статья посвящена обратному методу Маслова, который подходит для автоматизации доказательств в различных логических исчислениях: логика высказываний, классическая логика первого порядка, интуиционистская логика, модальные логики и т. д. Приведен обзор основных публикаций по обратному методу, рассмотрено разработанное авторами исчисление обратного метода для интуиционистской логики первого порядка. Предложены адаптированные и оригинальные стратегии оптимизации для этого исчисления. Рассмотрены алгоритм логического вывода в полученном исчислении и разработанная на его основе программа автоматического доказательства теорем WhaleProver. Приведены результаты сравнения разработанной программы с существующими аналогами на задачах из библиотеки ILTP.
Ключевые слова: автоматическое доказательство теорем, логический вывод, обратный метод, метод Маслова, интуиционистская логика.
Тип публикации: Статья
УДК: 004.832.32
Образец цитирования: В. А. Павлов, B. Г. Пак, “Экспериментальная программа для доказательства теорем интуиционистской логики обратным методом Маслова”, Научно-технические ведомости СПбГПУ. Информатика. Телекоммуникации. Управление, 2015, № 6(234), 70–80
Цитирование в формате AMSBIB
\RBibitem{PavPak15}
\by В.~А.~Павлов, B.~Г.~Пак
\paper Экспериментальная программа для доказательства теорем интуиционистской логики обратным методом Маслова
\jour Научно-технические ведомости СПбГПУ. Информатика. Телекоммуникации. Управление
\yr 2015
\issue 6(234)
\pages 70--80
\mathnet{http://mi.mathnet.ru/ntitu137}
\crossref{https://doi.org/10.5862/JCSTCS.234.7}
Образцы ссылок на эту страницу:
  • https://www.mathnet.ru/rus/ntitu137
  • https://www.mathnet.ru/rus/ntitu/y2015/i6/p70
    • Citing articles in Google Scholar: Russian citations, English citations
    Related articles in Google Scholar: Russian articles, English articles
    		Информатика, телекоммуникации и управление
    Статистика просмотров:
    Страница аннотации:154
    PDF полного текста:86
     
      Обратная связь:
    		  Пользовательское соглашение  Регистрация посетителей портала  Логотипы © Математический институт им. В. А. Стеклова РАН, 2025