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

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

Правила РШТ выражают принцип негативной интроспекции в следующей интерпретации: если выполняется формула 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 =

Имеем множество литералов 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. Таким образом, каждый отрицательный литерал должен быть истинным, тогда как положительным литералам достаточно быть доказуемыми. Из вышеизложенного можно заключить, что устойчивые мо- дели формируются из голов логической про- граммы, а значит, {a, b, c, d} никак не может быть устойчивой моделью программы P1. Таким образом, в семантике ASP шагом вывода будем называть построение устойчивой модели по имеющемуся на каждом шаге множеству убеждений.

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

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

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

Процесс вывода в РШТ можно разделить на следующие основные этапы (рис. 1):

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

-     трансляция входной теории в логическую программу ASP (в синтаксисе clingo);

-     обработка логической программы при помощи системы вывода clingo;

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

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

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

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

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

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

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

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

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

Представим пример входных данных, написанных на языке, заданном грамматикой анализатора (каждое правило вида 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-файл, дальнейшие шаги запуска clingo и модификации множества убеждений в процессе решения. Из листинга видно, какие факты и на каком шаге часов были получены. Пример демонстрирует обработку литералов later в правилах РШТ в соответствии с часами модели. Поскольку литерал d был успешно выведен на шаге часов 5, на шаге часов 7 стало выполнимо правило !later(10) ^ d => passed, приводящее к успешному (по смыслу примера) решению.

В результате разбора входного файла с РШТ T3 первоначально создается lp-файл, который затем модифицируется на каждом шаге решения. Начальное и конечное состояния lp-файла представлены на рисунке 2.

Результирующий файл results.txt будет следующим:

clingo version 5.5.2

Reading from ast_asp.lp

Solving...

Answer: 1

res(c) res(d) res(f) res(passed)

SATISFIABLE

Models     : 1

Calls      : 1

Time       : 0.002s (Solving: 0.00s

1st Model: 0.00s Unsat: 0.00s)

CPU Time   : 0.000s

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

Заключение

В работе была предложена архитектура решателя РШТ логики высказываний. Описан процесс разработки прототипа решателя, соответствующего предложенной архитектуре.

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

Рассмотрен пример, демонстрирующий поэтапный (пошаговый) процесс решения РШТ.

Предложенные программные средства зарегистрированы в реестре программ для ЭВМ РФ, свидетельство № 2021681551, и являются первой и уникальной реализацией системы вывода РШТ.

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

Работа выполнена при финансовой поддержке проектов РФФИ № 20-57-00015 Бел а, 20-07-00498.

Литература

1.    Панов А.И. Целеполагание и синтез плана поведения когнитивным агентом // Искусственный интеллект и принятие решений. 2018. № 2. С. 21–35. DOI: 10.14357/20718594180202.

2.    Furber R., Mardare R., Mio M. Probabilistic logics based on Riesz spaces. LMCS, 2020, vol. 16, iss. 1. DOI: 10.23638/LMCS-16(1:6)2020. URL: https://lmcs.episciences.org/6054 (дата обращения: 24.02.2022).

3.    Aldini A., Curzi G., Graziani P., Tagliaferri M. Trust evidence logic. Proc. ECSQARU, Lecture Notes in Computer Science, 2021, vol. 12897, pp. 575–589. DOI: 10.1007/978-3-030-86772-0_41.

4.    Mitani Y., Kobayashi N., Tsukada T. A probabilistic higher-order fixpoint logic. Proc. V Int. Conf. FSCD, 2020, vol. 167, art. 19, pp. 19:1–19:22. DOI: 10.4230/LIPIcs.FSCD.2020.19.

5.    Rybakov V. Temporal multi-valued logic with lost worlds in the past // Сибирские электронные математические изв. 2018. Т. 15. С. 436–449.

6.    Гнатенко А.Р., Захаров В.А. О выразительных возможностях некоторых расширений линейной темпоральной логики // Моделирование и анализ информационных систем. 2018. Т. 25. № 5. С. 506–524. DOI: 10.18255/1818-1015-2018-5-506-524.

7.    Elgot-Drapkin J., Perlis D. Reasoning situated in time I: Basic concepts. J. of Experimental and Theoretical Artificial Intelligence, 1990, vol. 2, pp. 75–98. DOI: 10.1080/09528139008953715.

8.    Fominykh I., Eremeev A., Alekseev N., Gulyakina N. Decision making and control of a cognitive agent’s knowledge process under time constraints. In: Communications in Computer and Information Science, 2020, pp. 212–221. DOI: 10.1007/978-3-030-60447-9_13.

9.    Fominykh I., Vinkov M. Paraconsistency of argumentation semantics for stepping theories of active logic. Proc. I Int. Sci. Conf. IITI’16, 2016, vol. 1, pp. 171–180. DOI: 10.1007/978-3-319-33609-1_15.

10. Vinkov M., Fominykh I. Stepping theories of active logic with two kinds of negation. Advances in Electrical and Electronic Engineering, 2017, vol. 15, no. 1, pp. 84–92. DOI: 10.15598/AEEE.V15I1.1990.

11. Fominykh I., Vinkov M. Step theories of active logic and extended logical programs. In: Advances in Intelligent Systems and Computing, pp. 192–201. DOI: 10.1007/978-3-319-68321-8_20.

12. Gelfond M., Lifschitz V. The stable model semantics for logic programming. In: ICLP/SLP, 1988, pp. 1070–1080.

13. Gebser M., Kaminski R., Kaufmann B., Schaub T. Multi-shot ASP solving with clingo. Theory and Practice of Logic Programming, 2019, vol. 19, no. 1, pp. 27–82. DOI: 10.1017/S1471068418000054.

References

1. Panov A.I. Goal setting and behavior planning for cognitive agent. Artificial Intelligence and Decision Making, 2018, no. 2, pp. 21–35. DOI: 10.14357/20718594180202 (in Russ.).
2. Furber R., Mardare R., Mio M. Probabilistic logics based on Riesz spaces. LMCS, 2020, vol. 16, iss. 1. DOI: 10.23638/LMCS-16(1:6)2020. Available at: https://lmcs.episciences.org/6054 (accessed February 24, 2022).
3. Aldini A., Curzi G., Graziani P., Tagliaferri M. Trust evidence logic. Proc. ECSQARU, Lecture Notes in Computer Science, 2021, vol. 12897, pp. 575–589. DOI: 10.1007/978-3-030-86772-0_41.
4. Mitani Y., Kobayashi N., Tsukada T. A probabilistic higher-order fixpoint logic. Proc. V Int. Conf. FSCD, 2020, vol. 167, art. 19, pp. 19:1–19:22. DOI: 10.4230/LIPIcs.FSCD.2020.19.
5. Rybakov V. Temporal multi-valued logic with lost worlds in the past. Siberian Electronic Mathematical Reports, 2018, vol. 15, pp. 436–449.
6. Gnatenko A.R., Zakharov V.A. On the expressive power of some extensions of linear temporal logic. Modeling and Analysis of Information Systems, 2018, vol. 25, no. 5, pp. 506–524. DOI: 10.18255/1818-1015-2018-5-506-524 (in Russ.).
7. Elgot-Drapkin J., Perlis D. Reasoning situated in time I: Basic concepts. J. of Experimental and Theoretical Artificial Intelligence, 1990, vol. 2, pp. 75–98. DOI: 10.1080/09528139008953715.
8. Fominykh I., Eremeev A., Alekseev N., Gulyakina N. Decision making and control of a cognitive agent’s knowledge process under time constraints. In: Communications in Computer and Information Science, 2020, pp. 212–221. DOI: 10.1007/978-3-030-60447-9_13.
9. Fominykh I., Vinkov M. Paraconsistency of argumentation semantics for stepping theories of active logic. Proc. I Int. Sci. Conf. IITI’16, 2016, vol. 1, pp. 171–180. DOI: 10.1007/978-3-319-33609-1_15.
10. Vinkov M., Fominykh I. Stepping theories of active logic with two kinds of negation. Advances in Electrical and Electronic Engineering, 2017, vol. 15, no. 1, pp. 84–92. DOI: 10.15598/AEEE.V15I1.1990.
11. Fominykh I., Vinkov M. Step theories of active logic and extended logical programs. In: Advances in Intelligent Systems and Computing, pp. 192–201. DOI: 10.1007/978-3-319-68321-8_20.
12. Gelfond M., Lifschitz V. The stable model semantics for logic programming. In: ICLP/SLP, 1988,
    pp. 1070–1080.
13. Gebser M., Kaminski R., Kaufmann B., Schaub T. Multi-shot ASP solving with clingo. Theory and Practice of Logic Programming, 2019, vol. 19, no. 1, pp. 27–82. DOI: 10.1017/S1471068418000054.