На правах рекламы:
ISSN 0236-235X (P)
ISSN 2311-2735 (E)

Авторитетность издания

ВАК - К1
RSCI, ядро РИНЦ

Добавить в закладки

Следующий номер на сайте

2
Ожидается:
16 Июня 2024

В Институте динамики систем и теории управления им. В.М. Матросова разработан метод трансляции первопорядковых логических формул в позитивно-образованные формулы.

09.01.2020

Для тестирования программной системы автоматического доказательства теорем (прувера), основанной на ПОФ-исчислении, использовалась библиотека задач TPTP (Thousands of Problems for Theorem Provers). Формат, в котором представлены задачи TPTP (называемые проблемами), де-факто стал стандартом среди сообщества, изучающего автоматизацию рассуждений. Возникает естественная необходимость в том, чтобы разрабатываемый прувер принимал на вход задачи в этом формате. Таким образом, возникла задача трансляции формул логики предикатов первого порядка, представленных в формате TPTP, в формат ПОФ. Эта задача нетривиальна из-за особой структуры формул ПОФ-исчисления. Предложенный (в сравнении с ранее разработанным алгоритмом в первой реализации системы автоматического доказательства теорем для ПОФ-исчисления) метод трансляции формул первопорядкового языка исчисления предикатов с сохранением исходной эвристической структуры знаний более эффективен, а его упрощенная версия для задач представлена на языке дизъюнктов.

Подробное описание дается в статье «Метод трансляции первопорядковых логических формул в позитивно-образованные формулы», авторы Давыдов А.В., Ларионов А.А., Черкашин Е.А. (Институт динамики систем и теории управления им. В.М. Матросова, Иркутск).