Software & Systems

Система поддержки истинности, основанная на предположениях (ATMS), является мощным инструментом поддержки логического вывода и наряду с достоверными фактами использует в своей работе факты, истинность которых неопределенна или на данном этапе неочевидна (множество предположений) [1, 2]. За счет сохранения информации о происхождении сделанных выводов и анализа возникающих противоречий ATMS удается отсекать те подмножества предположений, которые были сделаны неверно.

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

Подобное представление ATMS показало хорошие результаты, позволив диагностической системе работать с неполными входными данными (поиск мест для дополнительного снятия показаний) и с противоречивыми данными (данные из заведомо неисправной диагностируемой системы, противоречащие исходной модели, – поиск причины противоречия, неисправности) и значительно сузить пространство логического вывода [3, 4].

Дальнейшее исследование позволило расширить область применения ATMS в качестве поддержки логического вывода систем диагностирования класса произвольных сложных стационарных интеграционных систем.

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

Недостатком полученного результата являлось жесткое ограничение, унаследованное разрабатываемой системой от классической ATMS: строгая ориентированность на логику высказываний. Действительно, обязательное требование классического алгоритма к пропозициональности логики, на основе которой построен логический вывод, приводит к существенным проблемам, связанным с невозможностью использования ATMS в большинстве существующих диагностических систем (они построены на основе логики предикатов), а также к значительному и необоснованному повышению размера базы логических правил, описывающей модель диагностируемой системы (для описания перехода от одного состояния системы к другому требуется уникальное правило) [5, 6].

Вышеозначенные проблемы практически полностью нивелируют  преимущества от использования ATMS, которые были выявлены на предыдущих этапах исследования.

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

Описание ATMS

Охарактеризуем работу ATMS следующим образом [4, 7]:

–      задано множество правил хорновского вида;

–      заданы значения (определена заведомая истинность) некоторых утверждений, являющихся посылками правил.

Определение 1:  продукцией хорновского типа (хорновской продукцией) является правило вида a1&a2&…&an®b, где a1, …, an – посылки; b – результаты (заключения).

Определение 2: фактом называется утверждение, чья истинность точно определена.

Определение 3: предположением называется утверждение с неопределенной истинностью, однако временно принятое истинным.

Сделаем предположения об истинности нескольких утверждений, истинность которых еще не определена.

Основным материалом для обработки системы поддержки истинности являются метки утверждения.

Определение 4: меткой утверждения является множество предположений, на основе которых это утверждение выведено (множество поддержки утверждения).

Для меток утверждений верно следующее [8]:

–      метка заведомо истинных утверждений всегда пуста (записывается как <утверждение>{});

–      утверждение, являющееся предположением, поддерживает само себя (<утверждение> {<имя предположения>});

–      метка утверждения может состоять из нескольких множеств;

–      если утверждение не поддерживается ни одним из предположений, его метка неопределенна (<утверждение>{Æ});

–      противоречивые множества записываются как поддержка утверждения-противоречия ^ (утверждения Nogood).

Замечание 1: утверждение Nogood выделяется для удобства обработки противоречивых множеств предположений. Все операции, производимые над обычными утверждениями, аналогично производятся и над утверждением Nogood.

Определим условия применимости правил вывода:

–     посылка условно истинна, если ее множество поддержки определено; таким образом, условно истинными являются предположения и утверждения, полученные на основе предположений в ходе вывода; формально к условно истинным также относят и заведомо истинные утверждения, так как их метка, хотя и является пустой, но все же определена;

–     правило применимо, если все его посылки условно истинны;

–     поддержкой результата применимого правила является объединение множеств поддержки его посылок;

–     если в ходе логического вывода получены результаты, противоречащие заведомо истинным фактам, поддержка  этих результатов является противоречивой.

Опишем правила минимизации меток [4, 8].

Rule 1. Любое множество предположений, содержащее противоречивое множество, противоречиво.

Rule 2. Противоречивое множество предположений не может быть поддержкой утверждения. Если поддержка метки содержит противоречивое множество предположений, это множество может быть удалено.

Rule 3. Поддержка утверждения не должна быть избыточной: если метка противоречивого утверждения содержит два множества предположений A и B, причем AÎB, тогда множество B может быть удалено из метки.

Пример 1. Рассмотрим пример, иллюстрирующий процесс минимизации меток.

Пусть в ходе рассуждения стало известно, что некоторый факт S поддерживается множествами B={A1, A2, A3} и С={A2, A3, A4}, причем известно, что множество D={A3, A4, A5} противоречиво.

От системы поддержки истинности приходит сообщение о противоречивости множества предположений E={A3, A4} и о том, что факт S поддерживается множеством F={A1, A2}. Таким образом, после добавления полученных сведений состояние системы принимает следующий вид:

S{{A1, A2, A3}, {A1, A2}, {A2, A3, A4}},

^{{A3, A4, A5}, {A3, A4}}.

Видно, что множество E={A3, A4} содержится во множествах С={A2, A3, A4}, D={A3, A4, A5}. Значит, множества C и D могут быть удалены из поддержки соответствующих меток (Rule 3). Более того, множество F={A1, A2} полностью входит в множество B={A1, A2, A3}, а значит, мно- жество B также может быть удалено из метки, поддерживающей факт S (Rule 2). В итоге после применения правил минимизации состояние системы будет выглядеть следующим образом:

S{{A1, A2}}, ^{{A3, A4}}.

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

Алгоритм ATMS

Основной идеей ATMS является то, что в процессе вывода система может делать предположения об истинности подмножества утверждений, чья истинность становится условной. Оперируя предположениями и полученными на их основе выводами, система способна находить множества, содержащие ложные предположения, и локализовывать предположения, сделанные ошибочно [8].

Алгоритм ATMS представляет собой итерационное добавление утверждений о диагностируемой системе, поиск противоречивых множеств поддержки, добавление и обновление меток и анализ следующего места снятия показаний (предложение определения истинности наиболее подходящего утверждения, если такое возможно).

Формально это описание выглядит следующим образом.

Дано: связь с рассуждающей системой, поставляющей новые утверждения для обработки, множество сделанных предположений.

Требуется: найти противоречивое подмножество предположений, то есть множество предположений, сделанных неверно.

atms:

начало:

пока не найдена причина противоречия

[найти наиболее подходящее место для снятия показания];

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

добавить новое утверждение (add_sentence(утвер­ждение, {}));

выдать причину противоречия;

конец.

Примечание 1: критерий причины противоречия выбирается в зависимости от задачи; точным критерием является мощность противоречивого множества: если поддержка утверждения ^ содержит множество из одного элемента, то это предположение и является причиной противоречия.

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

Процедура добавления нового утверждения add_sentence имеет следующий вид.

Дано: добавляемое утверждение, полученное в процессе рассуждения, и его метка (множество поддержки).

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

add_sentence(утверждение,метка):

начало:

проверить, есть ли противоречие:

если да –

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

добавить утверждение в базу знаний;

применить правила минимизации меток;

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

для результата каждого применимого правила выполнить процедуру добавления утверждения add_sentence(утверждение,метка);

конец.

Проверка на наличие противоречия заключается в следующем: содержится ли одинаковое множество поддержки в метках взаимоисключающих утверждений. Простейшим примером является добавление заведомо истинного утверждения ({}): если уже существует обратное ему утверждение, то метка, поддерживающая его, является противоречивой.

Процедура минимизации меток заключается в процессе последовательного применения правил минимизации.

Поиском применимых правил занимается блок логического вывода: это может быть простая процедура перебора или процедура с эвристическими элементами.

Использование в ATMS фундаментальных примеров  в качестве предположений

Рассмотрим принципы ATMS. Несмотря на то что ATMS позиционирует себя как система, поддерживающая вывод в пропозициональной логике, в описании ее работы пропозициональность практически не используется. Действительно, ATMS не является системой логического вывода, это – надстройка над выводом, позволяющая делать предположения, собирать информацию о предположениях, на основе которых были сделаны те или иные выводы, и анализировать получаемые противоречия. В информации о том, как делаются выводы, система ATMS не нуждается.

Основная проблема использования ATMS в логике предикатов первого порядка – что взять в качестве предположений. В логике высказываний в качестве предположений авторы использовали элементарные высказывания, в логике предикатов им соответствуют эрбрановские фундаментальные примеры, то есть предикаты, в которых каждой из переменных было присвоено конкретное значение из универсума Эрбрана [2].

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

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

Использование в ATMS предикатов в качестве предположений

Основной проблемой использования предикатов в качестве предположений ATMS является то, что в отличие от классического логического вывода, где истинность предиката P(x1, x2, …, xn) определяется истинностью его фундаментальных примеров, в ATMS при использовании P(x1, x2, …, xn) в качестве предположения возможны его две различные интерпретации: предположение как общезначимый предикат и как объединение предположений, являющихся фундаментальными примерами, на заданной области определения.

Первая интерпретация означает, что предположение P(x1, x2, …, xn) истинно тогда и только тогда, когда истинны все его фундаментальные примеры, то есть, как только будет найдено хоть одно ложное значение P(a1, a2, …, an), предположение считается ложным. Предположение может быть записано, как P(x1, x2, …, xn) {P(x1, x2, …, xn)}.

Вторая интерпретация означает, что предположение P(x1, x2, …, xn) является лишь записью, объединяющей множество всех предположений – фундаментальных примеров на области определения переменных x1, …, xn. Таким образом, нахождение ложного значения P(a1, a2, …, an) означает лишь, что для конкретного значения переменных предположение было сделано неверно, в то время как для остальных значений это может быть и не так. Предположение в таком случае может быть записано как P(x1, x2, …, xn) {P(x1, x2, …, xn) {[v(xi)ÎU]/[v(xi)=ai]}}, где в форме «{[]}» записывается область, на которой верно предположение; при этом запись «v(xi)ÎU» означает, что предположение верно для любого значения переменной xi из универсума Эрбрана U, в то время как запись «v(xi)=ai» означает истинность предположения лишь для конкретного значения ai переменной xi, а знаком «/» будем обозначать подмножества значений, исключенных из области определения предположения.

Пример 2. Пусть имеются два предположения:

–      P1(x, y){P1(x, y)} – как общезначимый предикат ("x "y P(x, y));

–      P2(x, y){P2(x, y){[v(x)ÎU, v(y)ÎU]}} – как объединение предположений – фундаментальных примеров на области всех значений из универсума Эрбрана.

Пусть также было получено утверждение A(x, y){{P1(x, y)}, {P2(x, y){[v(x)ÎU, v(y)ÎU]}}}, которое независимо поддерживается обоими предположениями.

В ходе вывода было получено заведомо истинное утверждение Ø A(a, b){}.

Возникшее противоречие A(x, y){{P1(x, y)}, {P2(x, y)[v(x)ÎU, v(y)ÎU]}}, Ø A(a,b){} разрешимо: метка {{P1(x, y)}, {P2(x, y){[v(x)=a, v(y)=b]}}} противоречива.

Определим поддержку противоречивого утверждения как ^{{P1(x, y)}, {P2(x, y) {[v(x)=a, v(y)=b]}}}, а затем исключим противоречивые множества предположений (согласно правилу Rule 2 минимизации меток) из поддержки следующих утверждений, имеющихся в базе знаний:

–      P1(x, y) {Æ},

–      P2(x, y) {P2(x, y) {[v(x)ÎU, v(y)ÎU]/[v(x)=a, v(y)=b]}},

–      A(x, y) {P2(x, y) {[v(x)ÎU, v(y)ÎU]/[v(x)=a, v(y)=b]}}.

Заметим, что предположение {P1(x, y)} было добавлено в поддержку противоречивого утверждения, что говорит о ложности соответствующего предиката "x " yP(x, y), и было полностью удалено из поддержки всех утверждений, что, в свою очередь, указывает на недостоверность всех утверждений, сделанных на его основе.

В то же время предположение {P2(x, y) {[v(x)ÎU, v(y)ÎU]}} было внесено в поддержку противоречивого утверждения лишь частично ({P2(x, y) {[v(x)=a, v(y)=b]}}), что говорит о ложности лишь конкретного значения предиката P2(a, b), следовательно, должны быть пересмотрены только те утверждения, которые опираются лишь на предположение {P2(a, b)} или, что то же самое, {P2(x, y) {[v(x)=a, v(y)=b]}}.

Стоит отметить, что использование обеих интерпретаций обоснованно: в случае, когда требуется убедиться, что предикат P(x1, x2, …, xn) истинен не для всех значений переменных (при диагностическом выводе это может быть предикат «Исправен(элемент_устройства)»), тогда первая интерпретация (на основе общезначимого предиката) даст ответ за меньшее количество шагов (применения правил вывода). Однако, если тре- буется определить, какие конкретные значения предиката являются ложными (какие именно элементы работают неисправно), необходимо использовать вторую интерпретацию (на основе объединения предположений).

Если при использовании первой интерпретации ATMS, как и в случае использования в качестве предположений одиночных фундаментальных примеров, не претерпевает значительных изменений (они касаются лишь конкретной реализации функций «проверить, есть ли противоречие»), то для второй интерпретации требуется внести изменения, связанные с процессом означивания переменных.

Алгоритм ATMS – atms_pred_exists – для случая объединения предположений – фундаментальных примеров.

Дано: связь с рассуждающей системой, поставляющей новые утверждения для обработки, множество сделанных предположений.

Требуется: найти противоречивое подмножество предположений, то есть множество предположений, сделанных неверно.

Atms_pred_exists:

начало:

пока не найдена причина противоречия

[найти наиболее подходящее место для снятия показания];

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

добавить новое утверждение (add_sentence(утвер­ждение, {},значения_переменных));

выдать причину противоречия;

конец.

Процедура добавления нового утверждения add_sentence_all имеет следующий вид.

Дано: добавляемое утверждение, полученное в процессе рассуждения, и его метка (множество поддержки).

Требуется: добавить утверждение в базу знаний, обработать противоречия, актуализировать базу знаний по итогам обработки.

add_sentence_all(утверждение,метка,значения_перемен- ных):

начало:

проверить, есть ли противоречие:

если да –

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

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

добавить утверждение в базу знаний;

применить правила минимизации меток;

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

для результата каждого применимого правила выполнить процедуру добавления утверждения add_sentence(утверждение, метка, значения_пере­менных);

конец.

Подводя итоги, отметим, что в ходе исследования рассмотрены четыре способа применения ATMS:

–     в логике высказываний;

–     в логике предикатов с использованием фундаментальных примеров в качестве предположений;

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

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

Каждый из рассмотренных способов имеет свои положительные и отрицательные стороны.

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

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

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

Таким образом, каждый из рассмотренных приемов позволяет достигать корректного результата и обладает своими уникальными достоинствами. Это говорит о том, что каждый из них имеет право на жизнь, а за счет комбинирования различных подходов для решения конкретных задач можно достичь эффективных результатов.

Литература

1.    De Kleer J. An Assumption-based TMS, Artificial Intelligence, 1986, vol. 28, pp. 127–162.

2.    Вагин В.Н., Головина Е.Ю., Загорянская А.А., Фоми- на М.В. Достоверный и правдоподобный вывод в интеллектуальных системах: Монография. М.: Физматлит, 2008. 714 с.

3.    De Kleer J. Problem Solving with the ATMS. Artificial Intelligence, 1986, vol. 28, pp. 197–224.

4.    Вагин В.Н., Зарецкий Д.С. Система поддержки истинности на основе предположений в задачах диагностики с использованием модели устройств // AIS-IT’10: тр. конгресса по интеллект. сист. и информ. технологиям. М.: Физматлит, 2010. С. 351–362.

5.    De Kleer J., Mackworth A.K. and Reiter R. Characterizing diagnoses and systems. Artificial Intelligence, 1992, vol. 56, pp. 197–222.

6.    Вагин В.Н., Зарецкий Д.С. Решение задач диагностики с использованием систем поддержки истинности // Изв. ЮФУ (Технические науки: Интеллектуальные САПР). Таганрог: Изд-во ТТИ ЮФУ, 2010. № 12 (113). С. 63–71.

7.    Ngair Teow-Hin, Provan G. Focusing ATMS Problem-solving: a formal approach. Computer and Information Sc. Depart­ment Univ. of Pennsylvania Philadelphia, 1992.

8.    Kenneth D. Forbus, de Kleer J. Problem Solvers. MIT Press, 1993.

References

1.     De Kleer J. An Assumption-based TMS. Artificial Intelli­gence. 1986, vol. 28, pp. 127–162.

2.     Vagin V.N., Golovina E.Yu., Zagoryanskaya A.A., Fomi­na M.V. Dostoverny i pravdopodobny vyvod v intellektualnykh sistemakh [Reliable and reasonable output in intelligent systems]. Moscow, Fizmatlit Publ., 2008, 714 p.

3.     De Kleer J. Problem Solving with the ATMS. Artificial Intelligence. 1986, vol. 28, pp. 197–224.

4.     Vagin V.N., Zaretskiy D.S. Assumption-based truth main­tenance system in model-based diagnostics. Trudy kongressa po intellektualnym sistemam i informatsionnym tekhnologiyam “AIS-IT’10” [Proc. of congress on intelligent systems and IT “AIS-IT’10”]. Moscow, Fizmatlit Publ., 2010, pp. 351–362 (in Russ.).

5.     De Kleer J., Mackworth A.K., Reiter R. Characterizing diagnoses and systems. Artificial Intelligence. 1992, vol. 56, pp. 197–222.

6.     Vagin V.N., Zaretskiy D.S. Solving diagnostics problems using truth maintenance system. IZVESTIYA SFedU. ENGINEER­ING SCIENCES. Tematicheskiy vypusk “Intellektualnye SAPR” [News]. Taganrog, TTI Sib. Fed. Univ. Publ., 2010, no. 12 (113), pp. 63–71 (in Russ.).

7.     Ngair T.-H., Provan G.  Focusing ATMS Problem-solving: a formal approach. Computer and Information Science Dep., Univ. of Pennsylvania Publ., Philadelphia, 1992.

8.     Forbus K.D., de Kleer J. Problem Solvers, MIT Press, 1993.