Детальная информация

Название Эффективная программная реализация обратного метода Маслова для интуиционистской логики // Научно-технические ведомости Санкт-Петербургского государственного политехнического университета. Сер.: Информатика. Телекоммуникации. Управление: научное издание. – 2017. – Т. 10, № 1
Авторы Павлов Владимир Александрович
Выходные сведения Санкт-Петербург: Изд-во Политехн. ун-та, 2017
Коллекция Общая коллекция
Тематика Радиоэлектроника ; Искусственный интеллект. Экспертные системы ; метод Маслова ; Маслова метод ; интуиционистская логика ; обратные методы (логика) ; логические исчисления ; логические выводы ; автоматическое доказательство теорем ; method Maslova ; Maslova method ; intuitionistic logic ; inverse methods (logic) ; logical calculus ; logical conclusions ; automatic theorem proving
УДК 004.8
ББК 32.813
Тип документа Статья, доклад
Тип файла PDF
Язык Русский
DOI 10.18721/JCSTCS.10104
Права доступа Свободный доступ из сети Интернет (чтение, печать, копирование)
Ключ записи RU\SPSTU\edoc\40154
Дата создания записи 14.08.2017

Разрешенные действия

Прочитать Загрузить (0,9 Мб)

Группа Анонимные пользователи
Сеть Интернет

Изложены результаты исследования, посвящённого применению обратного метода Маслова для автоматизации логического вывода в интуиционистских логических исчислениях. Подробно рассмотрены адаптированные стратегии поиска вывода для интуиционистских исчислений обратного метода, а также новые стратегии, позволяющие ограничить возникающие переборы и уменьшить размер пространства поиска вывода. Также описаны детали реализации компьютерной программы, использующей обратный метод для логического вывода в интуиционистской логике первого порядка. Приведены результаты экспериментального сравнения предложенных стратегий друг с другом и новые результаты сравнения программы WhaleProver с существующими аналогами.

This paper contains the results of the research related to Maslov's inverse method and its application to first-order intuitionistic logic. Several proof search strategies for the inverse-method intuitionistic calculus, which allow reducing the proof search space and avoiding redundant inferences, are proposed and explained in detail. Some strategies are new, others are adapted variants of the existing strategies for classical logic. This article includes a detailed description of the automated theorem-proving system WhaleProver for first-order intuitionistic logic, which is based on the inverse method.

Место доступа Группа пользователей Действие
Локальная сеть ИБК СПбПУ Все
Прочитать Печать Загрузить
Интернет Все

Количество обращений: 559 
За последние 30 дней: 6

Подробная статистика