РОССИЙСКАЯ ФЕДЕРАЦИЯ
ФЕДЕРАЛЬНАЯ СЛУЖБА ПО ИНТЕЛЛЕКТУАЛЬНОЙ СОБСТВЕННОСТИ
ГОСУДАРСТВЕННАЯ РЕГИСТРАЦИЯ ПРОГРАММЫ ДЛЯ ЭВМ

Номер регистрации (свидетельства): 2016615547

Дата регистрации: 26.05.2016

Номер и дата поступления заявки: 2016612689 28.03.2016

Дата публикации: 20.06.2016

Контактные реквизиты:
E-mail: vlapav239@gmail.com
	
Автор:
Павлов Владимир Александрович

Правообладатель:
Павлов Владимир Александрович

Название программы для ЭВМ:
Программа для автоматического доказательства теорем в интуиционистских логических исчислениях обратным методом Маслова «WhaleProver» (WhaleProver)

Реферат:
Программа предназначена для автоматического установления выводимости формул в секвенциальных интуиционистских исчислениях высказываний и предикатов и может быть использована преподавателями и студентами в рамках учебного курса «Математическая логика», а также интегрирована в существующие системы искусственного интеллекта. Программа позволяет считывать из файла исходную формулу, применять выбранную модификацию обратного метода Маслова для установления выводимости формулы (в ряде случаев также может быть установлена её невыводимость), сохранять в файл доказательство в случае установления выводимости. В программе реализована возможность комбинировать следующие стратегии оптимизации логического вывода, позволяющие ограничивать возникающие переборы: стратегия поглощения секвенций, стратегия упрощения немаксимальных секвенций, ряд стратегий удаления «бесполезных» (недопустимых) секвенций, тактика расклеек, П-тактика, оптимизация правил сокращения (склеек).

Тип реализующей ЭВМ: IBM РС-совмест. ПК

Язык программирования: Visual С++ 2010, С++

Вид и версия операционной системы: Windows 7

Объем программы для ЭВМ: 489 Кб