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

Павлов, Владимир Александрович. Эффективная программная реализация обратного метода Маслова для интуиционистской логики [Электронный ресурс] / В. А. Павлов. — Электрон. текстовые дан. (1 файл : 900 Кб) // Научно-технические ведомости Санкт-Петербургского государственного политехнического университета = St. Petersburg state polytechnical university journal. Computer science. Telecommunications and control systems. Сер.: Информатика. Телекоммуникации. Управление: научное издание, 2017. – Т. 10, № 1 [Электронный ресурс]. — Загл. с титул. экрана. — Электронная версия печатной публикации. — Свободный доступ из сети Интернет (чтение, печать, копирование). — Текстовый файл. — Adobe Acrobat Reader 7.0. — <URL:http://elib.spbstu.ru/dl/2/j17-345.pdf>. — <URL:http://doi.org/10.18721/JCSTCS.10104>.

Дата создания записи: 14.08.2017

Тематика: Радиоэлектроника; Искусственный интеллект. Экспертные системы; метод Маслова; Маслова метод; интуиционистская логика; обратные методы (логика); логические исчисления; логические выводы; автоматическое доказательство теорем; method Maslova; Maslova method; intuitionistic logic; inverse methods (logic); logical calculus; logical conclusions; automatic theorem proving

УДК: 004.8

ББК: 32.813

Коллекции: Общая коллекция

Ссылки: DOI

Разрешенные действия: Прочитать Загрузить (0,9 Мб) Для чтения документа необходим Flash Player

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

Сеть: Локальная сеть ИБК СПбПУ

Аннотация

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

Права на использование объекта хранения

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

Статистика использования документа

stat Количество обращений: 0
За последние 30 дней: 0
Подробная статистика