Книжная полка Сохранить
Размер шрифта:
А
А
А
|  Шрифт:
Arial
Times
|  Интервал:
Стандартный
Средний
Большой
|  Цвет сайта:
Ц
Ц
Ц
Ц
Ц

Программные продукты и системы, 2022, том 35, № 2

международный научно-практический журнал
Бесплатно
Основная коллекция
Артикул: 787387.0001.99
Программные продукты и системы : международный научно-практический журнал. - Тверь : НИИ Центрпрограммсистем, 2022. - Т. 35, № 2. - 141 с. - ISSN 0236-235X. - Текст : электронный. - URL: https://znanium.ru/catalog/product/1895851 (дата обращения: 28.03.2024)
Фрагмент текстового слоя документа размещен для индексирующих роботов. Для полноценной работы с документом, пожалуйста, перейдите в ридер.
Научно-исследовательский институт

«Центрпрограммсистем»

Программные

продукты и системы

МЕЖДУНАРОДНЫЙ НАУЧНЫЙ ЖУРНАЛ

2022, том 35, № 2

(год издания тридцать пятый)

Главный редактор

Г.И. САВИН, академик РАН

SOFTWARE & SYSTEMS

International research journal

2022, vol. 35, no. 2

Editor-in-Chief 

G.I. SAVIN, Academician of the Russian Academy of Sciences

Research Institute CENTERPROGRAMSYSTEM

 ПРОГРАММНЫЕ ПРОДУКТЫ И СИСТЕМЫ
Международный научный журнал 

2022. Т. 35. № 2
DOI: 10.15827/0236-235X.138

Главный редактор 

Г.И. САВИН, академик РАН

Научные редакторы номера:

А.Н. Сотников, д.ф.-м.н., профессор 

А.П. Еремеев, д.т.н., профессор

Издатель НИИ «Центрпрограммсистем»

(г. Тверь, Россия)

Учредитель В.П. Куприянов

Журнал зарегистрирован в Роскомнадзоре 3 марта 2020 г.

Регистрационное свидетельство ПИ № ФС 77-77843

Подписные индексы в каталогах

Почты России ПП879

Урал-Пресс 70799

ISSN 0236-235X (печатн.)
ISSN 2311-2735 (онлайн)

МЕЖДУНАРОДНАЯ РЕДАКЦИОННАЯ КОЛЛЕГИЯ

Семенов Н.А. – заместитель главного редактора, д.т.н., профессор Тверского государственного технического 
университета (г. Тверь, Россия)
Сотников А.Н. – заместитель главного редактора, д.ф.-м.н., профессор, заместитель директора 
Межведомственного суперкомпьютерного центра РАН (г. Москва, Россия)
Афанасьев А.П. – д.ф.-м.н., профессор Московского физико-технического института (технического университета), 
заведующий Центром распределенных вычислений Института проблем передачи информации РАН (г. Москва, Россия)
Баламетов А.Б. – д.т.н., профессор Азербайджанского научно-исследовательского и проектно-изыскательского института 
энергетики (г. Баку, Азербайджан)
Батыршин И.З. – д.т.н., профессор Мексиканского института нефти (г. Мехико, Мексика)
Голенков В.В. – д.т.н., профессор Белорусского государственного университета информатики и радиоэлектроники 
(г. Минск, Беларусь)
Елизаров А.М. – д.ф.-м.н., профессор Института математики и механики им. Н.И. Лобачевского Казанского федерального 
университета (г. Казань, Россия)
Еремеев А.П. – д.т.н., профессор Национального исследовательского университета «МЭИ» (г. Москва, Россия)
Кузнецов О.П. – д.т.н., профессор Института проблем управления РАН (г. Москва, Россия)
Курейчик В.М. – д.т.н., профессор Инженерно-технологической академии Южного федерального университета 
(г. Таганрог, Россия)
Лисецкий Ю.М. – д.т.н., генеральный директор «S&T Ukraine» (г. Киев, Украина)
Мамросенко К.А. – к.т.н., доцент Московского авиационного института (национального исследовательского университета), 
руководитель Центра визуализации и спутниковых информационных технологий НИИСИ РАН (г. Москва, Россия)
Мейер Б. – доктор наук, профессор, заведующий кафедрой Высшей политехнической школы – ETH (г. Цюрих, Швейцария)
Нгуен Тхань Нги – д.ф.-м.н., профессор, проректор Ханойского открытого университета (г. Ханой, Вьетнам)
Николов Р.В. – доктор наук, профессор Университета библиотековедения и информационных технологий Софии
(г. София, Болгария)
Палюх Б.В. – д.т.н., профессор Тверского государственного технического университета (г. Тверь, Россия)
Рахманов A.A. – д.т.н., профессор, заместитель генерального директора Концерна «РТИ Системы» (г. Москва, Россия)
Серов В.С. – д.ф.-м.н., профессор Университета прикладных наук Оулу (г. Оулу, Финляндия)
Сулейманов Д.Ш. – академик АН Республики Татарстан, д.т.н., профессор Казанского государственного технического 
университета (г. Казань, Республика Татарстан, Россия)
Татарникова Т.М. – д.т.н., доцент, профессор Санкт-Петербургского государственного электротехнического университета 
«ЛЭТИ» им. В.И. Ульянова (Ленина) (г. Санкт-Петербург, Россия)
Ульянов С.В. – д.ф.-м.н., профессор, ведущий научный сотрудник Объединенного института ядерных исследований 
(г. Дубна, Россия)
Хорошевский В.Ф. – д.т.н., профессор Московского физико-технического института (технического университета) 
(г. Москва, Россия)
Язенин А.В. – д.ф.-м.н., профессор Тверского государственного университета (г. Тверь, Россия)

АССОЦИИРОВАННЫЕ ЧЛЕНЫ РЕДАКЦИИ

Национальный исследовательский университет «МЭИ», г. Москва, Россия
Технологический институт Южного федерального университета, г. Таганрог, Россия
Тверской государственный технический университет, г. Тверь, Россия

АДРЕС ИЗДАТЕЛЯ И РЕДАКЦИИ 
Россия, 170024, 
г. Тверь, просп. Николая Корыткова, д. 3а
Телефон (482-2) 39-91-49
Факс (482-2) 39-91-00
E-mail: red@cps.tver.ru
Сайт: www.swsys.ru

Дата выхода в свет 16.06.2022 г.

Отпечатано ООО ИПП «Фактор и К»

Россия, 170100, г. Тверь, ул. Крылова, д. 26

Выпускается один раз в квартал

Год издания тридцать пятый 

Формат 6084 1/8. Объем 140 стр.

Заказ № 12. Тираж 1000 экз. Цена 330,00 руб.

 SOFTWARE & SYSTEMS 
International research journal

2022, vol. 35, no. 2
DOI: 10.15827/0236-235X.138

Editor-in-chief 

G.I. SAVIN, Academician of RAS

Science editors of the issue:

A.N. Sotnikov, Dr.Sc. (Physics and Mathematics), Professor

A.P. Eremeev, Dr.Sc. (Engineering), Professor

Publisher Research Institute 

CENTERPROGRAMSYSTEM (Tver, Russian Federation)

Founder V.P. Kupriyanov

The journal is registered with the Federal Service 

for Supervision of Communications, Information Technology 

and Mass Communications (Roskomnadzor)

March 3rd, 2020

Registration certificate ПИ № ФС 77-77843

ISSN 0236-235X (print)

ISSN 2311-2735 (online)

INTERNATIONAL EDITORIAL BOARD

Semenov N.A. – Deputy Editor-in-Chief, Dr.Sc. (Engineering), Professor of the Tver State Technical University
(Tver, Russian Federation)
Sotnikov A.N. – Deputy Editor-in-Chief, Dr.Sc. (Physics and Mathematics), Professor, Deputy Director
of the Joint Supercomputer Center of the Russian Academy of Sciences (Moscow, Russian Federation)
Afanasiev A.P. – Dr.Sc. (Physics and Mathematics), Professor of the Moscow Institute of Physics and Technology, 
Head of Centre for Distributed Computing of Institute for Information Transmission Problems 
(Moscow, Russian Federation)
Balametov A.B. – Dr.Sc. (Engineering), Professor of the Azerbaijan Scientific-Research & Design-Prospecting Power 
Engineering Institute (Baku, Azerbaijan)
Batyrshin I.Z. – Dr.Sc. (Engineering), Professor of the Mexican Petroleum Institute (Mexico City, Mexico)
Golenkov V.V. – Dr.Sc. (Engineering), Professor of the Belarusian State University of Informatics and Radioelectronics 
(Minsk, Republic of Belarus)
Elizarov A.M. – Dr.Sc. (Physics and Mathematics), Professor of the N.I. Lobachevsky Institute of Mathematics 
and Mechanics of the Kazan Federal University (Kazan, Russian Federation)
Eremeev A.P. – Dr.Sc. (Engineering), Professor of the National Research University “Moscow Power Engineering 
Institute” (Moscow, Russian Federation)
Kuznetsov O.P. – Dr.Sc. (Engineering), Professor of the Institute of Control Sciences of the Russian Academy 
of Sciences (Moscow, Russian Federation)
Kureichik V.M. – Dr.Sc. (Engineering), Professor of the Academy of Engineering and Technology of the Southern
Federal University (Taganrog, Russian Federation)
Lisetsky Yu.M. – Dr.Sc. (Engineering), CEO of S&T Ukraine (Kiev, Ukraine)
Mamrosenko K.A. – Ph.D. (Engineering), Associate Professor of the Moscow Aviation Institute (National Research
University), Head of the Center of Visualization and Satellite Information Technologies SRISA RAS 
(Moscow, Russian Federation)
Meyer B. – Dr.Sc., Professor, Head of Department in the Swiss Federal Institute of Technology in Zurich, ETH 
(Zurich, Switzerland)
Nguyen Thanh Nghi – Dr.Sc. (Physics and Mathematics), Professor, Vice-Principal of the Hanoi Open University
(Hanoi, Vietnam)
Nikolov R.V. – Full Professor of the University of Library Studies and Information Technology (Sofia, Bulgaria)
Palyukh B.V. – Dr.Sc. (Engineering), Professor of the Tver State Technical University (Tver, Russian Federation)
Rakhmanov A.A. – Dr.Sc. (Engineering), Professor, Deputy CEO of the Concern RTI Systems
(Mosсow, Russian Federation)
Serov V.S. – Dr.Sc. (Physics and Mathematics), Professor of the Oulu University of Applied Sciences (Oulu, Finland)
Suleimanov D.Sh. – Academician of TAS, Dr.Sc. (Engineering), Professor of the Kazan State Technical University
(Kazan, Republic of Tatarstan, Russian Federation)
Tatarnikova T.M. – Dr.Sc. (Engineering), Associate Professor, Professor of the St. Petersburg Electrotechnical 
University "LETI" (St. Petersburg, Russian Federation)
Ulyanov S.V. – Dr.Sc. (Physics and Mathematics), Professor of the Dubna International University for Nature, 
Society and Man (Dubna, Russian Federation)
Khoroshevsky V.F. – Dr.Sc. (Engineering), Professor of the Moscow Institute of Physics and Technology
(Moscow, Russian Federation)
Yazenin A.V. – Dr.Sc. (Physics and Mathematics), Professor of the Tver State University (Tver, Russian Federation)

ASSOCIATED EDITORIAL BOARD MEMBERS

National Research University “Moscow Power Engineering Institute”, Moscow, Russian Federation
Technology Institute at Southern Federal University, Taganrog, Russian Federation
Tver State Technical University, Tver, Russian Federation

EDITORIAL BOARD AND PUBLISHER OFFICE ADDRESS 
Nikolay Korytkov Ave. 3а, Tver, 170024, Russian Federation
Phone: (482-2) 39-91-49  Fax: (482-2) 39-91-00
E-mail: red@cps.tver.ru

Website: www.swsys.ru

Release date 16.06.2022

Printed in printing-office “Faktor i K”

Krylova St. 26, Tver, 170100, Russian Federation

Published quarterly. 35th year of publication

Format 6084 1/8. Circulation 1000 copies

Prod. order № 12. Wordage 140 pages. Price 330,00 rub. 

Вниманию авторов

Международный журнал «Программные продукты и системы» публикует материалы научного и 

научно-практического характера по новым информационным технологиям, результаты академических и 
отраслевых исследований в области использования средств вычислительной техники. Практикуются выпуски 
тематических номеров по искусственному интеллекту, системам автоматизированного проектирования, 
по технологиям разработки программных средств и системам защиты, а также специализированные 
выпуски, посвященные научным исследованиям и разработкам отдельных вузов, НИИ, научных организаций. 


Решением Президиума Высшей аттестационной комиссии (ВАК) Министерства образования и науки 

РФ международный журнал «Программные продукты и системы» внесен в Перечень ведущих рецензируемых 
научных журналов и изданий, в которых должны быть опубликованы основные научные результаты 
диссертаций на соискание ученых степеней кандидата и доктора наук.

Информация об опубликованных статьях по установленной форме регулярно предоставляется в систему 
Российского индекса научного цитирования (РИНЦ), в CrossRef и в другие базы и электронные библиотеки.


Журнал «Программные продукты и системы» включен в ядро коллекции РИНЦ, размещенное на платформе 
Web of Science в виде базы данных RSCI.

Автор статьи отвечает за подбор, оригинальность и точность приводимого фактического материала.

При перепечатке ссылка на журнал обязательна. Статьи публикуются бесплатно.

Условия публикации

К рассмотрению принимаются оригинальные материалы, отвечающие редакционным требованиям и 

соответствующие тематике журнала (специализация – информатика, вычислительная техника и управление, 
отрасли науки – 05.13.01; .05; .06; .10; .11; .12; .15; .18; .19).

Работа представляется в электронном виде в формате Word. При обилии сложных формул обязательно 

наличие статьи и в формате PDF. Формулы должны быть набраны в редакторе формул Word (Microsoft 
Equation или MathType). Объем статьи вместе с иллюстрациями – не менее 10 000 знаков. Диаграммы, 
схемы, графики должны быть доступными для редактирования (Word, Visio, Excel). Все иллюстрации для 
полиграфического воспроизведения представляются в черно-белом варианте. Цветные, тонированные, от-
сканированные, не подлежащие редактированию средствами Word рисунки и экранные формы следует 
присылать в хорошем качестве для их дополнительного размещения на сайте журнала в макете статьи с 
доступом по ссылке. Заголовок должен быть информативным; сокращения, а также терминологию узкой 
тематики желательно в нем не использовать. Количество авторов на одну статью – не более 4, количество 
статей одного автора в номере, включая соавторство, – не более 2. Список литературы, наличие которого 
обязательно, должен включать не менее 10 пунктов.

Необходимы также содержательная структурированная аннотация (не менее 250 слов), ключевые сло-

ва (7–10) и индекс УДК. Название статьи, аннотация и ключевые слова должны быть переведены на ан-
глийский язык (машинный перевод недопустим), а фамилии авторов, названия и юридические адреса 
организаций (если нет официального перевода) – транслитерированы по стандарту BGN/PCGN. 

Вместе со статьей следует прислать экспертное заключение, лицензионное соглашение, а также сведе-

ния об авторах: фамилия, имя, отчество, название и юридический адрес организации, структурное подраз-
деление, должность, ученые степень и звание (если есть), контактный телефон, электронный адрес. 

Порядок рецензирования

Все статьи, поступающие в редакцию (соответствующие тематике и оформленные согласно требова-

ниям к публикации), подлежат двойному слепому рецензированию в течение месяца с момента поступле-
ния, рецензия отправляется авторам. 

В редакции сформирован устоявшийся коллектив рецензентов, среди которых члены международной 

редколлегии журнала, эксперты из числа крупных специалистов в области информатики и вычислительной 
техники ведущих вузов страны, а также ученые и специалисты НИИСИ РАН, МСЦ РАН (г. Москва) и НИИ 
«Центрпрограммсистем» (г. Тверь).

Редакция международного журнала «Программные продукты и системы» в своей работе руководству-

ется сводом правил Кодекса этики научных публикаций, разработанным и утвержденным Комитетом по 
этике научных публикаций (Committee on Publication Ethics – COPE).

Программные продукты и системы / Software & Systems
2 (35) 2022

145

УДК 621.398
Дата подачи статьи: 12.04.22, после доработки: 22.04.22

DOI: 10.15827/0236-235X.138.145-152
2022. Т. 35. № 2. С. 145–152

Разработка прототипа решателя 

для расширенных шаговых теорий логики высказываний

И.Б. Фоминых 1, д.т.н., профессор, fominykhIB@appmat.ru
Н.П. Алексеев 1, ст. преподаватель, AlekseevNP@mpei.ru
Н.А. Гулякина 2, к.ф.-м.н., доцент, зав. лабораторией, guliakina@bsuir.by
К.С. Кравченко 1, магистрант, KravchenkoKS@mpei.ru
М.В. Фомина 1, к.т.н., доцент, FominaMV@mpei.ru

1 Национальный исследовательский университет «МЭИ», г. Москва, 111250, Россия
2 Белорусский государственный университет информатики и радиоэлектроники 
(БГУИР), г. Минск, 220013, Беларусь

В настоящее время проводятся активные исследования возможностей использования неклассиче-

ских логик в моделировании рассуждений когнитивного агента.

В статье рассматривается проблема разработки и реализации прототипа решателя расширенных ша-

говых теорий в случае, когда решения по управлению сложным техническим объектом принимаются 
в условиях жестких временных ограничений. Рассматривается логическая система, основанная на ис-
пользовании шаговых теорий с двумя видами отрицания, – система расширенных шаговых теорий. 
Использование двух видов отрицания позволяет выводить как истинные факты, так и факты-убежде-
ния, что важно при моделировании рассуждений человека.

Основное внимание уделяется вопросу организации процедуры вывода на основе использования 

неклассических логик в моделировании рассуждений когнитивного агента. 

Приводятся основные этапы разработки прототипа расширенных шаговых теорий с использованием 

литералов логики высказываний. Для каждого компонента решателя описаны его функции, задачи, 
входные и выходные данные. Обоснован выбор системы вывода clingo, поддерживающей формирова-
ние расширенных логических программ Answer Set Programming (ASP) как инструмента реализации 
решателя. 

Приведены алгоритмы трансляции расширенных шаговых теорий в логическую программу, соот-

ветствующую синтаксису ASP. При организации логического вывода использован алгоритм цикличе-
ской обработки множеств убеждений расширенных шаговых теорий в среде clingo. Основные этапы 
работы этого алгоритма рассмотрены на примере, где разбираются этапы работы решателя и приводятся 
результаты, представленные в синтаксисе clingo. Пример работы решателя демонстрирует основные 
особенности расширенных шаговых теорий в задачах жесткого реального времени, такие как отказ 
от логического всеведения, самопознание и темпоральная чувствительность. 

В дальнейшем планируется рассмотреть применимость созданного решателя к более сложной формальной 
системе – логике предикатов первого порядка.

Ключевые слова: расширенная шаговая теория, решатель, активная логика, ограничения по времени, 
логическое программирование.

При моделировании рассуждений, связанных 
с обработкой временных зависимостей, в 
частности, в многоагентных системах [1], важным 
является понятие когнитивного агента. 
Подходы к организации логических рассуждений 
агента, происходящих во времени, рассматривались 
в работах [2–6]. Они представляют 
собой рассуждения о времени, то есть
внесение в правила вывода темпоральных литералов 
и правил их обработки. В данной работе 
рассматривается другой подход к рассуждениям 
когнитивного агента – рассуждения во 
времени, предполагающий соотнесение ре-
зультатов логического вывода агента с момен-
тами времени, в которые они были получены. 

Базовыми для концепции рассуждений во 

времени можно назвать формализмы активной 
логики (АЛ) – концептуальной системы, объ-
единяющей в себе ряд формализмов рассужде-
ний, происходящих во времени, которые рас-
сматриваются как протекающий во времени 
процесс [7]. Формализмы, отвечающие прин-
ципам АЛ, подходят для решения задач управ-
ления рассуждениями в условиях жестких вре-
менных ограничений [8], когда превышение 
допустимого количества времени на решение, 
называемого порогом, может приводить к ката-
строфическим последствиям. Рассуждения, 
удовлетворяющие данной концепции, обла-
дают следующими важными свойствами: во-

Программные продукты и системы / Software & Systems
2 (35) 2022

146

первых, результаты рассуждений могут быть
соотнесены с моментами времени, в которые 
они были получены, и когнитивный агент спо-
собен это осознавать (свойство темпоральной 
чувствительности), и, во-вторых, эти рассужде-
ния толерантны к возникающим в процессе 
рассуждения противоречиям (паранепротиво-
речивость). В работе [9] предложена паране-
противоречивая аргументационная семантика 
для формализма шаговых теорий (ШТ), объ-
единяющего в себе принципы АЛ и логиче-
ского программирования. В дальнейшем был 
разработан представленный в [10] более общий 
вариант формализма, содержащий два вида от-
рицания –
расширенные шаговые теории 

(РШТ). В работе [11] было выполнено соотне-
сение РШТ и расширенных логических про-
грамм, основанных на семантике ответных 
множеств (Answer Set Programming, ASP), ко-
торые, как известно, являются частными случа-
ями теорий с умолчаниями Р. Рейтера. 

В данной работе представлено дальнейшее 

развитие формализма РШТ с использованием 
ASP. Предложена архитектура решателя для 
ШТ, содержащих в правилах лишь пропозици-
ональные литералы. Разработан действующий 
прототип решателя, использующий в качестве 
модулей существующие системы вывода ASP.

РШТ как формализм, 

отвечающий принципам АЛ

Для моделирования рассуждений в систе-

мах жесткого реального времени существует 
необходимость использования темпорально 
чувствительных логик, так как в таких систе-
мах пренебрежение временем реакции на изме-
нения в окружающей среде неприемлемо. 
Кроме того, для задач управления сложными 
объектами в режиме жесткого реального вре-
мени характерно поступление новой, зачастую 
противоречивой информации, которую необ-
ходимо правильно обработать, чтобы время, 
отведенное на решение этих задач, не превы-
сило допустимый порог. АЛ позволяет рас-
сматривать рассуждения, происходящие во 
времени, не как статичную последовательность 
утверждений, a как протекающий во времени 
процесс. АЛ обладает несколькими интерес-
ными с точки зрения решаемой задачи особен-
ностями: отказ от логического всеведения, 
самопознание и темпоральная чувствитель-
ность [7].

Одной из систем АЛ являются ШТ. Множе-

ство правил ШТ разбиты на два подмножест-

ва – строгих и правдоподобных правил. В даль-
нейшем будем предполагать, что в теории при-
сутствуют только правдоподобные правила 
вида

N: a1  a2  …  am  b,
(1)

где N – имя правила; b – пропозициональный 
литерал; ai – пропозициональные литералы или 
литералы языка логики первого порядка вида 
later(j) или ¬later(j) (j – натуральное число, со-
поставленное определенному моменту времени). 
Эти правила означают, что если выполняется 
формула a1a2 … am и на данном шаге 
неизвестно, правдоподобна ли формула ¬b, то 
можно предположить, что формула b выполняется. 
Таким образом, система ШТ может рассматриваться 
как вариант системы активной 
логики, которая полностью основана на правилах 
и отвечает принципу логического программирования, 
в соответствии с которым моделями 
формул являются множества литералов, а 
не более сложные структуры в стиле Крипке.

Часы ШТ представляют собой конечную 

монотонно возрастающую подпоследовательность 
последовательности натуральных чисел, 
обозначенную далее Ck. Члены данной подпоследовательности 
характеризуют длительность 
последовательно выполняемых дедуктивных 
циклов, определяющих процесс рассуждения 
во всех системах АЛ [11]. 

Назовем ШТ пару T = (R, Ck), где R – конечное 
множество правил вида (1); Ck – конечная 
или бесконечная строго возрастающая подпоследовательность 
глобальных часов, члены которой 
являются моментами времени завершения 
дедуктивных циклов, называющаяся часами 
прогона модели.

Синтаксис расширенной ШТ отличается от 

синтаксиса других ШТ наличием в его алфавите 
языка правил оператора субъективного 
отрицания nott. Таким образом, правила будут 
иметь следующий вид:

N: a1  a2  …  am  nottc1  nottc2  … 

 nottcn  b,
(2)

где N – имя правила; b – пропозициональный 
литерал; a1, …, am – пропозициональные литералы 
или литералы языка логики первого порядка 
вида later(j) или ¬later(j) (j – натуральное 
число); c1, …, cn – пропозициональные литералы; 
nott – оператор субъективного отрицания. 
В отличие от оператора notx, обозначающего 
безуспешность попытки вывести литерал 
x средствами данной логической программы, 
выражение nottx в антецеденте правила РШТ 
означает, что агент не успел вывести литерал к 
текущему моменту времени.

Программные продукты и системы / Software & Systems
2 (35) 2022

147

Правила РШТ выражают принцип негативной 
интроспекции в следующей интерпретации: 
если выполняется формула a1  a2  … 
 am и на данном шаге вывода неизвестно, выполняется 
ли формула c1  c2 …  cn, то допустимо 
предположить, что выполняется формула 
b. При этом, как уже было сказано, –b
означает литерал, являющийся дополнением 
до контрарной пары для литерала b. 

Заметим, что между правилами РШТ и 

умолчаний в теориях с умолчаниями Р. Рейтера
имеется внешнее сходство. Соотношение РШТ
АЛ и расширенных логических программ, отвечающих 
семантике ответных множеств (как 
известно, являющихся частными случаями теорий 
с умолчаниями Р. Рейтера), рассмотрено в 
работе [11].

Логическое программирование ASP

Современным подходом к декларативному 

логическому 
программированию 
является 

ASP. Подход строится на понятии устойчивых 
моделей и семантике ответных множеств.

Логическая программа над набором атомов 

A представляет собой конечный набор правил r
следующего вида: a0  a1, … , am, am+1, … , 
an, где 0  m  n и каждый ai  A является атомом 
для 0  i n. Литералом называют атом ai
или его отрицание по умолчанию ai. Примем, 
что отрицание по умолчанию – это отсутствие 
информации об ai (формальная запись ai  X) 
в отличие от классического отрицания ai
(формально ai  X), где 𝑋 есть некоторая интерпретация.


Для каждого подобного правила r пусть
head(r) = a0 – голова правила;
body(r) = {a1, …, am, am+1, …, an} – тело

правила.

Тогда r интуитивно читается как head(r) –

истина, если выполняется body(r). В случае, 
если тело правила пусто, r назовем фактом.

Представим в качестве простого примера 

логическую программу P1:

P1 = 

,

,
,

,
.

a
c
b
d

d
a
c









Имеем множество литералов X, тогда пусть 

X+ = {p  A| p  X} и X- ={a  A|a  X}. Теперь
получим body(r)+ = {a1, …, am} и body(r)- = 
= {am+1, …, an}. 

Назовем правило r положительным, если 

body(r)- = . Соответственно, и логическая 

программа называется положительной, если 
все правила положительны. Набор атомов логической 
программы P обозначим как atom(P), 
а набор тел всех правил программы – body(P). 
Набор тел правил программы, имеющих схожую 
голову a, обозначим как bodyp(a) = 
= {body(r)|r  P, head(r) = a}.

Множество атомов X  A является моделью

программы P, если head(r)  X всякий раз, когда 
body(r)+  X и body(r)- X =  для каждого 
r  P. Таким образом, программа P1 имеет 
шесть моделей, среди которых выделим {a, c} 
и {a, b, c, d}. Модель называют минимальной, 
если никакое подмножество этой модели не является 
моделью программы [12].

В соответствии с семантикой устойчивых 

моделей, принятой в ASP [12], редукт PX программы 
P на множестве X определим как PX = 
= {head(r)  body(r)+|r  P, body(r)-  X = }, 
где PX является положительной программой, 
поэтому она имеет минимальную модель. Тогда 
X называют устойчивой моделью программы 
P, если X является минимальной моделью 
PX.

Проверим полученные модели программы

P1 на устойчивость:

X
P1X
минимальная 

модель P1X

{a, c}
P1{a, c} = 

= {a , c }

{a, c}

{a, b, c, d}
P1{a, b, c, d} =

= {a }

{a}

Видно, что {a, c} в отличие от {a, b, c, d}

является устойчивой моделью P1.

На практике редукт PX программы P на множестве 
X можно получить следующим образом:

− 
из программы удаляют все правила, содержащие 
в теле отрицание по умолчанию a
для a  X;

− удаляют также все литералы вида a из 

тел оставшихся правил.

Возвращаясь к примеру, заметим, что все 

атомы в модели {a, c} устойчивы к применению 
правил P1, в то время как для модели {a, b,
c, d} истинность атомов b, c и d не может быть 
установлена. В таком случае можно утверждать, 
что каждый атом устойчивой модели
доказуем правилами из P. Таким образом, каждый 
отрицательный литерал должен быть истинным, 
тогда как положительным литералам 
достаточно быть доказуемыми. Из вышеизложенного 
можно заключить, что устойчивые модели 
формируются из голов логической про-

Программные продукты и системы / Software & Systems
2 (35) 2022

148

граммы, а значит, {a, b, c, d} никак не может 
быть устойчивой моделью программы P1. Та-
ким образом, в семантике ASP шагом вывода 
будем называть построение устойчивой мо-
дели по имеющемуся на каждом шаге множе-
ству убеждений.

Существуют несколько активно развиваю-

щихся проектов программной реализации ASP, 
среди них наиболее современной системой вы-
вода для ASP-программ можно назвать си-
стему вывода clingo [13]. Она совмещает в себе 
граундер (программный компонент, который
отвечает за получение пропозиционального 
аналога логической программы, содержащей 
литералы логики первого порядка) и решатель.

Темпоральности РШТ при использовании 

системы вывода clingo можно достигнуть ите-
ративной обработкой правил (в соответствии с 
понятием шага применительно к изменению 
моментов времени на часах Ck). Основная 
сложность данного процесса заключается в об-
новлении множества известных фактов, кон-
троле непротиворечивости и управлении пра-
вилами с условиями вида later(t). 

Проектирование решателя

Процесс вывода в РШТ можно разделить на 

следующие основные этапы (рис. 1):

− анализ входной теории, разбор на со-

ставляющие подобъекты и создание объекта-
теории для последующей обработки системой;

− трансляция входной теории в логиче-

скую программу ASP (в синтаксисе clingo);

− обработка логической программы при 

помощи системы вывода clingo;

− получение результатов и дополнение су-

ществующего множества известных убежде-
ний;

− вывод полученного множества убежде-

ний.

Первые четыре этапа являются повторяю-

щимися и определяются часами прогона Ck об-
рабатываемой расширенной шаговой теории Т. 
Последний этап выполняется в конце работы 
решателя. 

На вход решателя поступает текстовый 

файл, содержащий описание РШТ в соответ-
ствии с синтаксисом, определенным анализа-
тором.

Архитектура решателя предполагает реали-

зацию перечисленных далее компонентов.

Анализатор является лексически-синтакси-

ческим, проверяет корректность синтаксиса 
РШТ и создает новый объект ШТ в системе вы-
вода.

Транслятор обрабатывает объект ШТ и 

формирует из него логическую ASP-програм-
му, отвечающую синтаксису решателя clingo. 

Сlingo используется в качестве подсистемы, 

вызываемой решателем для обработки имею-
щихся фактов и правил с целью получения но-
вого множества убеждений на конкретном 
шаге вывода.

Модификатор РШТ выполняет корректи-

ровку множества известных убеждений в соот-
ветствии с новыми результатами, а также вы-
полняет фильтрацию правил (отбрасывает пра-
вила, гарантированно не задействованные на 
текущем шаге, в соответствии с часами про-
гона модели, удаляет правила с субъективным 
отрицанием уже выведенного на предыдущих 
этапах моделирования факта в теле). 

РШТ

Транслятор

ASP-

программа

Множество 
убеждений

Итоговое 
множество 
убеждений

Анализатор

Входной файл 

РШТ

Clingo

Нет

Да

Есть еще шаги 

по часам?

Модификатор 

РШТ

Рис. 1. Процесс вывода итогового множества 

убеждений

Fig. 1. The process of deriving the final set 

of beliefs

Программные продукты и системы / Software & Systems
2 (35) 2022

149

Представим пример входных данных, напи-

санных на языке, заданном грамматикой анали-
затора (каждое правило вида a =>b соответ-
ствует тому факту, что из а выводимо b):

T3: {

R: {

=>a,
a =>c,
c =>d,
d =>f,
!later(10) ^ d => passed,
later(13) ^ not[t](passed) => failed

};

Ck = [0, 1, 3, 5, 7, 11]

}

Трансляция РШТ

В данный момент в логической программе 

присутствуют следующие виды объектов:

− have_facts(X): факты, известные реша-

телю в данный момент времени (аксиомы или 
полученные на предыдущих шагах разбора 
теории);

− possible_facts(Y): антецеденты правил, 

добавленных в процессе трансляции ШТ в ло-
гическую программу;

− conj(X, Y): отношение вывода из суще-

ствования объекта X объекта Y.

Модифицирующими правилами логической 

программы являются правила, определяющие 
состав ответного множества. В данный момент 
в решателе используется лишь правило вида
res(Y) :- have_fact(X), possible_fact(Y), conj(X, Y). 

Это правило отвечает за проверку, можно

ли достигнуть тела правила a => b на текущем 
шаге разбора шаговой теории. 

Обработка РШТ

При обработке РШТ начальное время на ча-

сах выставляется на третью позицию, так как в 
нулевой момент времени мы не знаем ничего, а 
при t = Ck[1] знаем только аксиомы. Потреб-
ность в обработке правил возникает только при 
t = Ck[2]. 

Если в правиле присутствует литерал 

later(ti) и tcur > ti, то добавляем антецедент A в 
множество possible_facts, формируем из остав-
шихся литералов правило вида conj(X, A) и за-
писываем его в файл.

Если в правиле присутствует литерал 

!later(ti) и tcur < ti, то добавляем антецедент A в 
множество possible_facts, формируем из остав-

шихся литералов правило вида conj(X, A) и записываем 
его в файл.

Если в правиле присутствует литерал 

not[t](fact), то добавляем антецедент A в множество 
possible_facts, формируем из оставшихся 
литералов правило вида conj(n_fact, A) и 
записываем его в файл. Записываем в логическую 
программу множество possible_facts в 
виде possible_facts(a; b; …).

Демонстрация работы решателя

Приведем листинг работы решателя для 

РШТ с именем T3, описанной ранее:

Запускаем анализатор
Разбор правил успешно завершен
Разбор таймера успешно завершен
Синтаксический анализ успешно завершен, 
расширенная теория T3 получена
Запущен процесс получения 'решения'
***************************************
Запущена новая итерация.

Текущее время: 3
Файл логической программы создан
Запускаю clingo
Результат получен
Добавлен новый факт: c
***************************************
***************************************
Запущена новая итерация.

Текущее время: 5
Файл логической программы создан
Запускаю clingo
Результат получен
Добавлен новый факт: d
***************************************
***************************************
Запущена новая итерация.

Текущее время: 7
Файл логической программы создан
Запускаю clingo
Результат получен
Добавлен новый факт: f
Добавлен новый факт: passed
***************************************
***************************************
Запущена новая итерация.

Текущее время: 11
Файл логической программы создан
Запускаю clingo
Результат получен
***************************************
Моделирование завершено
Итоговое множество: ['a', 'c', 'd', 'f', 
'passed']

На листинге показаны этапы анализа и 

трансляции в lp-файл, дальнейшие шаги за-