автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Разработка и реализация алгоритма обработки нечетких данных в многоуровневых логиках

ВВЕДЕНИЕ.

ГЛАВА I. ВВЕДЕНИЕ В ОБОБЩЕННУЮ ЛОГИКУ ПОСТА.

1.1. Множества логических значений.

1.2. Синтаксис и семантика.

1.2.1. Внутренний уровень.

1.2.2. Внешний уровень.

1.3. Секвенциальное исчисление.

1.3.1. Секвенции.

1.3.2. Вывод и правила вывода.

1.3.3. Теоремы и аксиомы.

ГЛАВА II. РАСПОЗНАВАНИЕ АКСИОМ ОБОБЩЕННОЙ ЛОГИКИ ПОСТА.

2.1. Подготовка и преобразование секвенции для тестирования.

2.2. Метод установления неразрешимости систем элементарных линейных неравенств.

2.2.1. Постановка задачи.

2.2.2. Преобразование системы.

2.2.3. Необходимое и достаточное условие неразрешимости систем элементарных линейных неравенств.

2.2.4. Доказательство необходимости условий неразрешимости.

2.2.5. Представление системы в виде графа.

2.2.6. Доказательство достаточности условий неразрешимости.

2.3. Алгоритм проверки разрешимости системы элементарных линейных неравенств.

2.4. Сложность алгоритма проверки разрешимости системы элементарных линейных неравенств.

2.5. Случай множества логических значений, несимметричного относительно нуля.

2.5.1. Доказательство взаимооднозначности преобразования множества значений.

2.5.2. Доказательство сохранения (не)совместности преобразованной системы.

2.5.3. Примеры преобразований несимметричного множества значений системы неравенств.

2.6. Алгоритм распознавания аксиом обобщенной логики Поста.

ГЛАВА III. ОПИСАНИЕ АЛГОРИТМА ПОИСКА ВЫВОДА.

3.1. Представление вывода.

3.2. Представление формул и секвенций.

3.2.1. Представление формул.

3.2.2.Представление секвенций.

3.3. Поиск пр авил и порядок их применения.

3.3.1. Выбор главного члена секвенции.

3.3.2.Поиск применимых правил.

3.3.3. Значение порядка применения правил.

3.3.4. Таблицы приоритетов выбора правил.

3.4. Кванторные правила и их ограничения.

3.4.1. Раскрытие кванторов и унификация.

3.4.2. Ограничения на подстановку. Параметры в кванторных правилах.

3.4.3. Усиление ограничений в кванторных правилах.

3.4.4. Домены для подстановки.

3.4.5. Стратегия замораживания повторяющихся кванторных формул и ограничения на число их раскрытий.

3.5. Схема алгоритма вывода.

3.6. Дополнительные опции вывода.

3.6.1. Выявление расширенных аксиом.

3.6.2. Стратегии проверки элементарных секвенций.

3.6.3. Установка параметров унификации.

3.7. Параметры алгоритма выявления аксиом.

ГЛАВА IV. ОПИСАНИЕ СИСТЕМЫ АВТОМАТИЧЕСКОГО ПОИСКА ВЫВОДА.

4.1. Структур а данных и реализация алгоритма.

4.1.1. Структура программы.

4.1.2. Представление данных.

4.1.3. Реализация основных частей алгоритма.

4.2. Общий вид и назначение системы.

4.3. Подготовка входных данных.

4.3.1. Настройка параметров логики.

4.3.2. Ввод исследуемой формулы.

4.4. Установка дополнительных параметров системы автоматического построения вывода.

4.4.1. Выбор стратегий.

4.4.2. Дополнительные настройки системы.

4.5. Задание имен входных и выходных файлов.

4.6. Запуск и работа основного алгоритма.

4.6.1. Автомагический режим вывода.

4.6.2. Интерактивный режим вывода.

4.7. Представление и просмотр результатов работы алгоритма.

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

При решении таких задач используются логические аппараты, позволяющие строить вывод и проверять выводимость формул этих логик. Для этих целей создаются различные компьютерные системы, автоматически строящие вывод в той или иной логике, так называемые автопруверы (automatic theorem provers).

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

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

Анализ и обобщение секвенциального аппарата многозначных логик Поста, а также их расширений позволил провести исследования в области организации поиска вывода и выбора стратегий построения доказательств. Кроме того, в работе рассмотрен аппарат проверки несовместности систем линейных неравенств, применяемый для определения аксиом обобщенной логики Поста. Также разработан и реализован алгоритм, строящий вывод в обобщенной логике Поста, расширенной операцией логического сравнения, которая позволяет сравнивать степени достоверности различных высказываний. Для этого алгоритма найдена стратегия поиска вывода, позволяющая значительно сократить время построения доказательства и объем дерева вывода.

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

Большинство существующих систем автоматического поиска вывода в логиках первого порядка, такие как Otter [14], Meteor, Isabelle, Vampire и другие, разработаны для работы в операционных системах Unix и Solaris, и не могут быть использованы в среде Windows, являющейся достаточно популярной в настоящий момент и широко используемой в учебном процессе. Разработанная система ASDS позволяет работать в операционной системе Windows, начиная с версии Windows 95.

По сравнению с табличными системами автоматического поиска доказательства, позволяющими строить выводы в многозначных логиках, представленная система не требует от пользователя ввода громоздких истинностных таблиц, описывающих операции и правила вывода в этих логиках. В качестве сравнения можно привести широко распространенный в зарубежных университетах пакет Deep Thought, описанный в [11]. Для того, чтобы с его помощью смоделировать обобщенную логику Поста на множестве всего из трех значений (например: -1, 0, 1), понадобилось бы сформировать и заполнить 32 таблицы, количество элементов в каждой из которых колебалось бы от 9 до 36. Предложенная же система не требует ввода такого количества информации, а основывается на заданных правилах вывода и границах введенного интервала логических значений, не зависимо от того, сколько таких значений будет рассмотрено. Скорость вывода в представленной системе также не уступает скорости, затрачиваемой на вывод секвенций в аналогичных системах, а при условии, что в разработанной системе не затрачивается время на ввод таблиц валентности для каждого логического оператора, общее время, затрачиваемое на исследование вывода одной секвенции, значительно сокращается.

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

Приведем краткий обзор содержания работы.

Диссертация состоит из четырех глав, и двух приложений.

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

Описаны два уровня рассматриваемой логики, внутренний и внешний. На внутреннем уровне в качестве атомов рассматриваются пропозициональные константы и предикаты. Принимаемые ими логические значения могут быть не только нулем и единицей (тождественной истиной и тождественной ложью), но также иметь степени градации истинности, то есть принимать значения из заданного множества логических величин, обозначаемого через L. В качестве такого множества L, например, могут быть рассмотрены все целые числа в промежутке от -10 до +10. Тогда все отрицательные значения будут интерпретироваться как ложные, все положительные - как истинные в той или иной степени (в зависимости от значения), а логическая константа ноль будет соответствовать парадоксальному значению. Заметим, что такие парадоксальные значения допустимы не во всех видах логик Поста, например, в четнозначной логике Поста использование парадоксальных значений запрещено.

Формулы внутренней логики образуются при помощи следующих операций традиционной логики Поста: конъюнкции, дизъюнкции, отрицания и кванторов. Разрешено также использование условного выражения if-then-else-Ji. Логические значения полученных формул также принадлежат к множеству L. Основной логической операцией, выполняемой над двумя внутренними, формулами является их сравнение. То есть еслир и q - формулы внутренней логики, то при помощи операций сравнения можно получить формулы вида р<д, p<q, p-q. Такие формулы называются логическими сравнениями и являются атомарными формулами внешней логики. Значения формул внешней логики двузначны: они могут быть истинными или ложными, в зависимости от логических величин сравниваемых внутренних формул. Внешняя атомарная формула p<q принимает значение "истина", когда логическое значение внутренней формулы р строго меньше логического значения внутренней формулы q. Аналогично определяются значения для остальных двух видов сравнений. Также как и в классической (двузначной) логике, из атомарных внешних формул с помощью классических булевых операций образуются расширенные внешние формулы.

В исчислении обобщенной логики Поста рассматриваются только безантецедентные секвенции, которые представляют собой цепочки формул внешней логики, начинающиеся знаком >". Например, следующая запись представляет се1свенцию в исчислении обобщенной логики Поста —> (a\jb)<(-c8ul), ~(a<d)&(c <b), (Зхр(х)<\).

Простейший вид, который может иметь секвенция в этой логике - это набор элементарных сравнений вида (p<q) или (p<q), где р и q являются внутренними атомарными формулами, возможно с отрицаниями. Такие секвенции будем называть элементарными. Приведем пример элементарной секвенции логики сравнений —> (а<Ь), (Ь<^а), (pb< 1). Под значением секвенции в заданной интерпретации понимается логическое значение классической дизъюнкции всех ее членов, в которых все переменные заменены значениями, согласно данной интерпретации. Секвенция, максимальная элементарная подсеквенция которой истинна в любой интерпретации, называется аксиомой.

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

Говорят также о выводимости внешней формулы А, подразумевая выводимость секвенции -»А.

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

В главе 2 приведен алгоритм, устанавливающий аксиоматичность заданной секвенции в обобщенной логики Поста [15].

Этот алгоритм использует метод проверки несовместности системы линейных неравенств с коэффициентами +1 и -1, описанный в [5]. Основная идея метода заключается в сопоставлении элементарной секвенции -Mfli<b {),. (an<bn), (c\<di),. (cm<dm) системы линейных неравенств S ={(b\<a\). (bn<an) (di<c{). (dm<cm)}, где at, bj для i е[1 .n\ и ch dj для j<=\\.m\ являются переменными или константами из множества L, возможно со знаком "минус". Реализованный в системе алгоритм, который устанавливает неразрешимость систем такого вида, основан на методе А.В. Тишкова [3]о представлении системы неравенств в виде нагруженного ориентированного графа с целью его дальнейшего исследования на предмет выявления в нем противоречий. Основные приемы, используемые в методе - это поиск и исследование компонент сильной связности этого графа, обход графа в ширину, а также отыскание в нем кратчайших путей.

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

Глава 3 подробно описывает основополагающий алгоритм построения вывода. Рассмотрены модели внутреннего представления формул, секвенций и метод организации самого вывода. Также приведены необходимые теоретические обоснования и примеры. В данной главе особо отмечена роль выбора стратегий вывода, в частности порядка применения правил. В [1] показано, что различная последовательность примененных правил может в значительной степени отражаться на длине и ширине дерева вывода, и предложена стратегия выбора правил в зависимости от вида обрабатываемых секвенций. В ходе апробации программы было проведено свыше 300 тестовых выводов, охватывающих возможные виды секвенций. В результате этого была создана база данных системы, на основании которой созданный алгоритм выбирает правило в создавшейся ситуации.

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

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

В главе 4 описаны структуры данных и основные процедуры реализации алгоритма, приведены фрагменты программного кода с объяснениями. Также отражены основные возможностей системы, описан ее интерфейс и предлагаемых в ней сервисы, среди которых можно перечислить как автоматический, так и "ручной" вывод исходной секвенции, проверку разрешимости систем элементарных линейных неравенств, возможность работы в многооконном текстовом редакторе, использование системы подсказок и прочее. Общее описание интерфейса системы приведено в [4].

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

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

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

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

Одна из основных задач алгоритма поиска вывода состоит в выборе на каждом шаге правила, позволяющего получить наименьшее дерево вывода (сократить длину вывода). Интересен тот факт, что если в классической логике для получения минимального дерева вывода всегда, по возможности, избегают ветвления секвенции, предпочитая увеличивать глубину дерева ради сокращения его ширины, то в обобщенной логике Поста это далеко не всегда так. Например, если при выводе формулы —> ( ~(C\/D) < (А&В)). откладывать применение "разветвляющего" правила до тех пор, пока это возможно, понадобиться применить 8 правил, в результате чего получится 4 элеменарных секвенции. Если же двухпосылочное правило использовать в самом начале, то для вывода этой формулы понадобиться 5 применений правил, а элементарных секвенций получится всего две. При увеличении длины формул разница длин выводов может возрастать экспоненциально.

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

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

Система создана с использованием языка Delphi версии 4.0, часть алгоритма для работы в системе DOS и Unix реализована с помощью Visual Prolog версии 4.0

Объем предоставленной реализации составляет приблизительн 8500 строк на языке Delphi. Объем объектного кода - примерно 700 КВ.

В приложениях приведены тестовые примеры и их решения, построенные в разработанной системе ASDS (Automated System for Sequent Derivation).

Среди основных результатов данной диссертационной работы можно отметить разработку оптимизирующей стратегии поиска вывода секвенций в обобщенной логике Поста, теоретическую доработку и реализацию алгоритма проверки разрешимости систем линейных неравенств специального вида, разработку и реализацию основного алгоритма построения вывода в обобщенной логике Поста и создание интегрированной интерактивной системы на основании этого алгоритма, опубликованных в [1], [4], [5] и [15].

вывода} if TavtChk=l then writeln(FileLgo,'--Immediate Axiom Testing Mode ON--'); if TavtChk=2 then writeln(FileLgo,1--Immediate Axiom and Extended Axiom

Testing Mode ON --');

NumberSecv:=l;

Deriveall(pS,elsecvlist,elSecvListQ); writeln(FileLgo); if (Strategy=l) and StopDerive {В случае, когда пользователем выбрана «быстрая проверка», при обнаружении условия, при котором исходная секвенция не может быть выведена, исследование секвенций в остальных узлах дерева вывода будет прекращено и процесс поиска вывода будет остановлен} then writeLn(FileLgo, 'Elementary not-axiom sequent was detected.

Derivation process has been stopped') else writesecvlist(elsecvlist,sT); if sT<>'' then writeln(FileLgo,'Elementary sequents list for axiom testing',sT); {запись в отчет списка элементарных секвенций на исследование} if (detailrap) and (AXlist<>nil) then begin writesecvlist(Axlist,sT); writeLn(FileLgo, '=== Axioms and Extended Axiom: ===',sT); end; Ax:=true; if Strategy=2 then begin Close(Fileln); Ax:=SystemCheck; end; if not Ax then NotAxiom:=true else begin if elSecvListQ<>nil then begin {case of quantifier existence} if Strategy=2 then begin AllAx:=true;

Assign(Fileln, fileINname); Append(Fileln); end; в случае кванторов, после их первого раскрытия запускается алгоритми унификации} Unif yall (MVList, elSecvListQ, pUniSet, Ax) ;

Repeat в случае, когда секвенция еще не выведена и содержит замороженные1 кванторы, они раскрываются повторно, пока пользователь не остановит процесс по соответствующему запросу системы) oldDegree:=CurFreeze; if CurFreeze<MaxFreeze then begin

NotAxiom: =not Ax; if not Ax then begin if Testmode then frmManDr.Show; QntRepeatQuest(MaxFreeze,CurFreeze); if CurFreeze>oldDegree then begin writeln(FileLgo); writeln(FileLgo, 'The initial sequent is not yet 'Frozen quatifier formulae will time (',CurFreeze,')'); writeln (FileLgo) ; elsecvlistNew:=nil;

Deriveplus(elsecvlistQ,elsecvlistNew); Unifyall(MVList,elsecvlistNew,pUniSet,Ax); derived.'+#13+ repeated one more

1 Стратегия замораживание повторяющихся квангорных формул описана в разделе 3.4.5 writeln(FileLgo,sT); donepDList(elsecvlistQ); elsecvlistQ:=elsecvlistNew; {donepDList(elsecvlistNew);} NotAxiom:= not Ax; end; end; end; until (CurFreeze=oldDegree) ; по окончании вывода производится очистка памяти} donepDList (elsecvlist) ; donepDList(elsecvlistQ) ; donejpDList(elsecvlistNew); end;

Close(Fileln); end; {if not axiom}

NotAxiom:= (elscvex and not AllAx) or N"otAxiom; EndWork; end;

4.2. Общий вид и назначение системы.

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

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

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

Заключение

Основными результатами диссертации являются: разработка оптимизирующей стратегии поиска вывода секвенций в обобщенной логике Поста;

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

Достоверность результатов подтверждена доказанными теоремами и более 1000 проведенных тестов.

1.. Косовский Н.К., Смирнова Е.С. Система автоматического построения вывода в классической и многоуровневой логиках // Седьмая международная конференция «Региональная Информатика -2000» (РИ-200) Труды конференции, СПб.: 200], с. 109-112.

2. Косовский Н.К., Тишков А.В. Логики конечнозначныхпредикатов на основе неравенств, Издательство Санкт-Петербургского Государственного Университета, 2000.

3. Косовский Н.К., Тишков А.В. Полиномиальные алгоритмы установления совместимости в рациональных и целых числах систем строгих и нестрогих линейных неравенств // Актуальные проблемы современной математики Т.З (1996),. с. 95-100

4. Смирнова Е.С. Система автоматического построения доказательств в классической и многоуровневой логике // Информатика исследования и инновации. Выпуск 5. Межвузовский сборник научных трудов - СПб: ЛГОУ им. А С. Пушкина, 2001. с.50.

5. Смирнова Е.С., Косовский Н.К. Алгоритм проверки разрешимости систем элементарных неравенств И Материалы четвертой молодежной школы по дискретной математике и ее приложениям. М:. Издательство МГУ, 2000. с. 74-81.

6. Шанин Н А., Давыдов Г.В., Маслов С.Ю., Минц Г.Е., Оревков В.П., Слисенко А О Алгорифм машинного поиска естественного логического вывода в исчислении высказываний, Издательство «Наука», 1965.

7. Aho А. V., Hopcroft J.E., Ullman J.E. The Design and Analysis of computer Algorithms, Addition-Weseley, Reading, MA, 1974.

8. Beauquier D., Kossovski N, Smirnova E. An Algorithm For Solvability Testing Of Elementary Linear Inequalities Systems./! 6th IMACS International Conference On Applications Of Computer Algebra, IMACS АСА 2000. pp. 59-61.

9. Defays D. Les foisonnements de I'intelligence artificielle. Liege Bruxelles, 1988.

10. Prince D. Algorithmes sur les graphes. Paris 1995. pp.127-135, 185-230.

11. Gerberding S. Deep Thought. University of Darmstadt, Dept. of Computer Science, 1996.

12. Lukasiewicz, J. Elementy logiki matematycznej, Warsaw: PWN, 1929; перевод О. Wojtasiewicz, Elements of Mathematical Logic, Oxford: Pergamon Press, 1963.

13. Lowerence C.Paulson. Designing a theorem Prover. Oxford, 1995. pp. 416-476.

14. Kalman J. A. Automated Reasoning with Otter, Rinton Press, 2001.

15. SmirnovaE. Using Symbolic Computation in an Automated Sequent Derivation System for Multi-valued Logic П J. Calmet, B. Benhamou, O. Caprotti, L. Henocque, V.Sorge

16. Eds ): Artificial Intelligence, Automated Reasoning, and Symbolic Computation Joint International Conference, AISC 2002 and Calculemus 2002 Marseille, France, My 1-5, 2002. Proceedings LNAI 2385, p64, ff. Marseille, France, 2002, pp. 64-75.

17. Taijan R. Data Structures and Network Algorithms, SIAM Philadelphia, 1983, 71-95.

18. Taijan R. Depth First Search and Linear Graph Algorithms, SIAM J. Computing 1 1972, 146-160.