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