Программные продукты и системы

Знание, являющееся общим для всех агентов, представлено на метауровне каждого агента А. с использованием предиката ALLKNOW (знают все). Для каждого агента А. мы вводим специальные аксиомы, позволяющие работать с этим знанием.Пусть Т.- какая-то теория объектного уровня агента А.: либо ownTi, либо TJi. Тогда all-reason: Vwlw2w3.ANSWERS(A..wl,dontknow) ^THEOREM(add(w2,add(w3,emptyT),wl)s ALLKNOW(w3) л ACCEPTVIEW(A.w2) =>THEOREM(Tfmknot(w2))     IЭта аксиома предназначена для вывода заключений, которые агент А может узнать и соотнести с другими агентами. Такие заключения могут выводиться из знаний, доступных всем агентам (выражаемых ALLKNOW), и ответов типа "я не знаю". При доказательстве all-reason будет использоваться агентом А3 для ввода в Т23 (т.е. в знание А3 об А2 ) результата рассуждения А2 об А1 .Доказательство, которое приводит к решению задачи о трех мудрецах, делается неформально. Ответ на вопрос "Какого цвета Ваш колпак?", обращенный к первому мудрецу, - просто попытка получить доказательства для THEOREM (ownT , 'white'). Поскольку попытка не удается, то А2 и А3 узнают ANSWERS (A ,'whitel',dontknow). С целью облегчения чтения доказательства употребляются выражения объектного уровня, заключенные в одиночные кавычки, которые используются в качестве имен на метауровне для соответствующих формул объектного уровня. Например, ‘┐(┐white2^ ┐white3)' стоит вместо mknot(mkand(mknot(white2),mknot(white3))), которая представляет собой метауровневое обозначение для выражения объектного уровня ┐(┐white2 ^ ┐white3). Для краткости в доказательстве atleast обозначаетформулу 'whitel V white2 v white3'.Второй мудрец рассуждает следующим образом:- ALLKNOW(atleast)- ANSWERS(A,'whitel',dontknow)- THEOREM(T\,'white2A ┐white3)')По аксиоме all-reason, применяемой к Т12, имеем 'whitel','┐white2^ ┐white3' и atleast. Условие THEOREM (add('┐white2^ ┐white3',add(atleast emptyT)),'whitel') может быть легко проверено, как uACCEPTVIEW (А1,'┐white2^ ┐white3').Заключение, полученное в результате рассуждений о знаниях общего характера, не вносит в Т1 новую информацию. Если мы предполагаем, что Т1 инициировано с теми знаниями, о которых А известно, что они известны А^ то Т'2 содержит white3, что соответствует тому факту, что и А , и А2 могут видеть колпак третьего агента. По той же причине не существует новой информации, которую можно было бы внести в собственные знания А2. В этот момент делается попытка доказать THEOREM(ownT^'white2'), и А? отвечает: "Я не знаю". Агент Аз отмечает, что ANSWERS (A'white2\ dontknow), и доказательство выводится следующим образом:- ALLKNOW(atleast)- ANSWERS(A}, 'whitel', dontknow)В этом месте А мог бы вывести в ownT , что ┐(┐white2^ ┐white3) но для доказательства это бесполезно. Вместо этого он рассуждает о знаниях, которыми, как ему известно, располагает А2.3 - THEOREM(T23 ,‘┐white2^ ┐white3)')По аксиоме all-reason, применяемой к А1 , имеются 'whitel','┐white2^ ┐white3' и atleast. Условие THEOREM(add('┐white2^ ┐white3',add(atleast emptyT)),'whitel') может быть легко проверено, так же, как и A CCEPTVIEW(A^,'┐white2^ ┐white3').В этом месте А замечает, что А не может дать определенного ответа и делает из этого вывод о цвете своего колпака.- ANSWERS(A2,'white2',dontknow)- KNOWS(A^'^(->white3)')По аксиоме reason, применяемой к А , имеются 'white2' и '-> w/шеЗ'. Условие THEOREM (add(' - white3\ ty, 'whiter) может быть легко проверено, так же, как и ACCEPTVlEW(Ai'-< whiter).- THEOREM(T23 , '┐(┐ white3)') по аксиоме knows.- THEOREM (own Т3 , ‘┐ ( ┐ white3)') по аксиоме confidence.Задача о трех мудрецах решалась в различных формальных системах, базирующихся на модальной логике [11, 19]. Она обсуждалась Coscia и др. в [9] в рамках системы, располагающей средствами для работы с базой знаний. Их решение представляет структуру из метаописаний, основанную на различных типах связей, которые могут быть установлены между теориями.Предлагаемая дедукция получается при помощи программы метауровня, написанной на расширенном Прологе. В этой архитектуре многие аспекты рассматриваются неявно. Например, последствия ответов "я не знаю", даваемых мудрецами, не выводятся в явной форме остальными, а просто утверждаются в каждой теории. Более того, внутри каждой теории нет различия между собственным знанием и знанием о других.Представленная архитектура основана на архитектуре [5] и является более общей и гибкой, чем схема, приведенная в [4]. В этом предложении знания, относящиеся i рассуждению о рассуждениях всех агентов, представлены в одном метаконтексте, а I знания объектного уровня каждого агента представлены в отдельном контексте, разбитом на "приватную" и "видимую" части. Приватное знание доступно тому агенту, который им владеет, а видимое знание доступно и другим агентам.Другое решение, основанное на логике хорновских предложений, было дано Nail Abdallah [25]. Вместо того, чтобы опираться на какую-то связь между знаниями объектного и метауровней, он использует специальные структуры, называемые ионами, для работы с локальностью доказательств. Интерпретация ионов не слишком поддается интуиции, хотя они и предназначены для моделирования операций метауровня, которые характеризуют рассуждения о знаниях и рассуждениях и позволяют избежать парадоксов, связанных с самоссылками. Мы придерживаемся стандартной семантики логики первого порядка, а проблемы, вызываемые самоссылками, не возникают из-за свойств механизма контекстов и явного контроля хода дедукции.Одно из решений задачи было дано в рамках системы OMEGA [6], в которой знания трех мудрецов представлены тремя точками зрения, а дедукция осуществляется в соответствии с некоторым множеством правил, которые определяют общие свойства таких точек зрения. Эта формализация ближе к нашей, но использованная е [6] аксиома Непрямого Доказательства, которая является свойством, соответствующим предположению о замкнутом мире, должна применяться к приемлемым позициям: так, второй мудрец не может предполагать, что первый знает цвет своего колпака, иначе возникает противоречие.Если представить агента как множество теорий (или систему контекстов, если придерживаться терминологии FOL), составляющих теорию метауровня, в которой представлено знание, относящееся к рассуждению о рассуждениях, и три теории объектного уровня для отображения собственных знаний агента и его сведений о других агентах, то нужно отметить, что такая организация не является специфической для структуры решаемой задачи. Связь между теориями объектного уровня и метатеорией устанавливается при помощи объединяющих правил, которые применяются неявным образом для постоянной поддержки собственных знаний агента в соответствии с заключениями, достигнутыми в метатеории. Этим объясняется то. что представление собственной системы доверия предполагается корректным, например тогда, когда агент отвечает на вопрос без рассуждений о знаниях и рассуждениях, а просто используя информацию, содержащуюся в его собственной теории. Наоборот, представление знаний других агентов обновляется явным образом в соответствии с предположением, что полученным заключениям следует доверять. Аксиома Knows, которая описывает это свойство, легко адаптируется к ситуации, где заключения, полученные в результате рассуждения о знаниях других агентов, нуждаются в дальнейшем подтверждении перед включением их в представление о других агентах.Аксиома confidence утверждает, что сам агент должен верить заключениям, полученным в результате рассуждения о других агентах, если они не противоречат его знаниям. Если агенты не являются лояльными друг к другу, можно смоделировать дополнительные условия, при которых агент должен поверить результатам рассуждений о знаниях другого агента.Аксиома reason рассматривает рассуждения, в результате которых некоторый агент может сделать вывод об информации, доступной другим агентам. Если инфор мацией, представленной другим агентом, является "я не знаю", то аксиома reason может быть прочтена как рассуждение о незнании других агентов. Формулировка этой аксиомы позволяет строить доказательства методом от противного. С другой стороны, гипотезы в гипотетическом рассуждении проблемно зависимы. Они не могут быть полностью произвольными, но должны подчиняться общему принципу: агент не должен делать предположений, противоречащим ответам других агентов.Архитектура агента представляет все знания, выраженные двумя уровнями операторов знаний, в явной форме. Иными словами, все предложения, включающие знания о знаниях других агентов, могут быть интерпретированы в терминах теорий объектного уровня, представленных внутри агента. В случае большего числа уровней описания знаний представление агента может быть расширено путем построения необходимых теорий на метауровне вместе с аксиомами для манипулирования.Описанная архитектура дает явное представление о базах знаний, допускающих рассуждения о знаниях других агентов: структура агента воплощает в себе структуру данных, представляющую такие знания как некую теорию объектного уровня. Базы знаний могут быть также неявно представлены на метауровне и построены явным образом лишь в случае их использования. Важным моментом при выборе варианта конструкции является вопрос о том, как представлять эти базы знаний, учитывая их размеры и частоту использования.В действительности задача о трех мудрецах могла быть решена просто с использованием общего знания, а не знаний агентов о других агентах. Все рассуждение целиком может быть построено от аксиомы atleast до ответов агентов. Представленное здесь решение направлено на использование более общей структуры рассуждений о знаниях и рассуждениях, поэтому подчеркиваются знания об агентах, а не только используемое общее знание. Это общее знание могло быть также представлено явным образом аналогично знанию о других агентах. Стоит отметить, что в метауровневой архитектуре системы FOL представление общего знания может быть совместным для агентов. Это позволяет избежать дублирования шагов доказательства, строящегося на общем знании.Степень общности архитектуры не полностью использована в решении задачи о трех мудрецах, поскольку все три агента очень похожи друг на друга. Архитектура может быть использована для формализации таких проблем, в которых каждый агент имеет собственное метазнание, отличное от других, и имеет собственную точку зрения на знания других. Представляется, что при использовании модальной логики с такой ситуацией справиться было бы нелегко.Хотя ситуация с произвольным числом агентов может быть отображена непосредственно, было бы полезно иметь более компактную характеристику множеств агентов, чьи знания И/ИЛИ поведения сходны. Для определения общих свойств агентов необходимы рассуждения о структурах и стратегиях дедукции, представленных на метауровне, что может быть достигнуто путем создания мета-метауровня. В принципе такого рода рассуждения реализовать легко, но на практике решить эту задачу не так-то просто. Например, свойство два агента имеют одинаковое представление о знаниях третьего агента может быть явно формализовано (на мета-метауровне) в терминах свойств (выражаемых на метауровне) представлений знаний агентов.Вот решение задачи о трех мудрецах, реализованное в системе FOL, которое близко к приведенному в основном тексте.Каждый агент А. реализован внутри FOL как система S., состоящая из метаконтекста и трех контекстов объектного уровня, соответствующих own Т. и двум TJ.. В аксиоматике FOL эти три объектных контекста представлены в моделирующей струх-туре соответствующего метаконтекста (эти три метаконтекста metal, meta2, metaЗ).Приведем полное определение третьего метаконтекста meta3 (NAMECONTEXT - назвать контекст). NAMECONTEXT тetaЗ;На метауровне имеются определения структур данных для манипулированиг правильно построенными формулами (wffs) и контекстами. Определение структура данных выводится путем декларирования символа, обозначающего сорт элементов из его области определения, - домене, констант, представляющих элемента домена, функциональных символов для операций с ними и символов переменных, пробегающих значения из определяемого сорта.DECLARE SORTAWFFWFF; MOREGENERAL WFF; DECLARE INDVAR w wl w2[WFF]; DECLARE INDCONSTwhite 1 white! white3\AWFF]; DECLARE INDCONST atleast black23[WFF];DECLARE FUNCONSTmkandmkormkimp{WFF,WFF) = WFF[INF\; DECLARE FUNCONST mknot(WFF) = WFF;Здесь4 определяется сорт правильно построенных формул (wffs) и атомарных правильно построенных формул (awffs). Команда MOREGENERAL строит решето определений сорта, причем в данном случае каждая атомарная правильна построенная формула является также и правильно построенной формулой. Символы w,wl и w2 представляют собой переменные, определенные на WFF, atleast и Ыаск23 - константы, представляющие правильно построенные формулы объектного уровня. Функции mkand, mkor, mkimp, mknot (взять логическое произведение, логическую сумму, логическую импликацию, логическое отрицание) являются правильно построенными формулами для нужных конструкторов, применение INF в квадратных скобках означает использование этих функций в инфиксном режиме.Это определение констант и конструкторов связывается в моделирующей структуре с каждым символом реализующей LISP - функции. Имена этих функций, используемые в моделирующей структуре, имеют префикс I, облегчающий интерпретацию. В то же время объекты, определенные п этой моделирующем структуре, используют для константных символов имена исходных символов . ATTACH whitel TO whitel; ATTACH white2 TO white2; ATTACH white3 TO white3; ATTACH mkand TO l-mkand; ATTACH mkor TO l-mkor; ATTACH mkimp TO l-mkimp; ATTACH mknot TO l-mknot; LET atleast = (whitel mkor white2)mkor white3;LET Blаск23 = mknot(white2)mkand mknot(white3);Команда системы LET связывает константные символы с левой стороны равенства с результатом вычисления выражения справа. В данном случае atleast определяется в моделирующей структуре в терминах формулы, представляющей, что один колпак - белый, а Ыаск23 - в терминах формулы, представляющей, что на втором (и третьем) мудреце черный, а не белый колпак.Дается определение структур данных для системы и контекстов . DECLARE SORT CONTEXT SYSTEM; DECLARE INDCONST SI S2[SYSTEM];DECLARE INDCONST CO emptyCownC3 C31 C32[CONTEXT]; DECLARE INDVARxC[CONTEXT];DECLARE FUNCONST declsentconst(AWFF,CONTEXT) = CONTEXT; DECLARE FUNCONST addfact(WFF,CONTEXT) = CONTEXT;Функция declsentconst получает правильно построенную атомарную формулу (один контекст) и возвращает новый контекст с декларацией некоторой сентенциальной константы. Это метауровневое описание действия команды DEC-LARESENTCONST, отданной на объектном уровне. Функция addfact получает на входе правильно построенную формулу, контекст и выдает новый контекст с новым фактом. Обе эти функции и константа emptyC определяются в терминах соответствующих элементов в нашей моделирующей структуре. Константа emptyC ассоциирована с LISP - структурой, представляющей пустой контекст. ATTACH emptyC TO emptyC; ATTACH declsentconst TO l-declsentconst; ATTACH addfact TO l-addfact;В дальнейшем эти команды для определения моделирующей структуры будут опускаться.DECLARE SORT ANSWER; DECLARE INDCONST yes no dontknow [ANSWER];Сорт ANSWER используется для представления ответов, даваемых мудрецами (например в предикате ANSWERS).В этой аксиоматизации необходимо использовать некоторые предикаты для формализации гипотез задачи и отношений между контекстами и системами7. DECLARE PREDCONST DEMO(CONTEXT, WFF); DECLARE PREDCONSTACCEPTVIEW(SYSTEM, WFF); DECLARE PREDCONST KNOW(SYSTEM, WFF); DECLARE PREDCONST A NSWERS(SYSTEM, WFF ANSWER); DECLARE PREDCONST HOLDS(WFF, CONTEXT); DECLARE PREDCONST ALLKNOW(WFF)Первые два предиката определены в моделирующей структуре. Предикат DEMO проверяет, может ли какая-то правильно построенная формула выводиться в этом контексте (DEMO заменяет предикат THEOREM, поскольку последний уже используется в специальном смысле в команде REFLECT). Предикат DEMO определяется в моделирующей структуре как системная процедура для выявления тавтологий. Предикат ACCEPTVIEW проверяет, является ли какая-то правильно построенная формула приемлемой с точки зрения некоторой системы: такая формула является приемлемой, если она не содержит ссылок на цвет колпак мудреца, отображаемого этой системой, поскольку сам мудрец не видит своего колпака. Например, ACCEPTVIEW(Sl,w) верно, если whitel не встречается в w. Предикаты KNOWS, ALLKNOW, ANSWERS являются эквивалентами предикатов. I которых уже говорилось. Для выражения правила связи между метаконтекстом и объектным контекстом необходимы предикат HOLDS (выполняется) и функции updatectx (обновить контекст). Чтобы избежать правил вывода, которые при попытке доказать w обращаются из контекста объектного уровня к метауровню в поисках доказательства HOLDS ('w',C), любой факт w, соответствующий аргумент} факта HOLDS ('w',C), утверждается на объектном уровне. Поэтому каждый раз, когда HOLDS\ ('w',C) выводится на метауровне, контекст С обновляется мере команду LET и функцию updatectx.DECLARE FUNCONST updatectx(CONTEXT, WFF); AXIOM updated xC.updatectx(xC, w) - IF HOLDS(w,xC) THEN addfact(w,xC) ELSExC;Декларации в metal и metal идентичны показанным с соответствующей сменой индексов для систем и контекстов.Контексты объектного уровня строятся при помощи команды LET, которая конструирует некоторую структуру данных и связывает ее с соответствующим символом метаконтекста. Для упрощения сначала определяется некоторый контекст СО, а затем на нем строятся все другие контексты. LET CO = declsentconst(white3,declsentconst(white2,declsentconst(whitel,emptyC)));После выполнения этой команды константный символ СО этого метаконтекста нашей моделирующей структуре имеет интерпретацию как структура данных, представляющая контекст с тремя сентенциальными константами (соответствующим! whitel, white2, white3).LET ownC3 - addfact(atleast,addfact(whitel,addfact(whitel,CO))); LET C31 = addfact(atleast,addfact(whitel,CO));LET 02 = addfact(atleast,addfact(whitel,CO));Контекст ownC3, C31, C31 описывает тот факт, что третий мудрец знает, чтя колпаки первых двух мудрецов белого цвета и что по крайней мере один из трех колпаков - белый. Он также знает, что двум другим мудрецам известно, что по крайне! мере один колпак - белый, и первый мудрец видит белый колпак на втором мудреце и наоборот. Аналогичные инструкции выполняются для создания объектных контекстов для систем S1 и S1.Здесь приводятся аксиомы метауровня для теtaЗ, идентичные тем, которые уже были использованы в вышеописанном решении. AXIOM knowsl: Vw. KNOWS(Sl,w) л-        DEMO(mknot(w), C31)=*HOLDS(w,C31);AXIOM knowsl: Vw. KNOWS(Sl,w) л-        DEMO(mknot(w), C31)=>HOLDS(w,C31);
AXIOM confidence 1: Vw. HOLDS(w,C31) л-. DEMO(mknot(w),ownC3) =*HOLDS(w,ownC3); AXIOM confidence!: Vw. HOLDS(w,C32) л- DEMO(mknot(w),ownC3) => HOLDS (w,ownC3); AXIOM reasonl: \/wlw2. ANSWERS(Sl,whitel,dontknow) ЛDEMO(addfact(w2,C31),wl) л ACCEPTVIEW(S1, w2) =>KNOWS(Sl,mknot(w2)); AXIOM reason2: VwlwZ ANSWERS(S2,white2,dontknow) лDEMO(addfact(w2,C32),wl) л A CCEPTVIEW(S2, w2) => KNOWS(S2,mknot(w2)); AXIOM all-reason 1: \fxC w wl w2.ANSWERS(Sl,whitel,dontknow) л DEMO(addfact(w2,addfact(w,emptyC),wl) л ALLKNOW(w) л Л CCEPTVIEW(S1, w2) =*· HOLDS(xQmknot(w2)); Этим завершается аксиоматизация для meta3. В других метаконтекстах аксиомы остаются такими же, если не считать новых имен для контекстов и систем.Если рассмотреть рассуждения трех мудрецов при попытке ответить на вопрос короля "Каков цвет Вашего колпака?", то можно сделать вывод, что рассуждение опирается на метауровневые дедукции. Здесь приводится доказательство (ниже FOL:: представляет собой запрос на ввод информации, поступающий от системы FOL; генерируемые факты пронумерованы в порядке их построения) . FOL:: SWITCHCONTEXTmeta1; FOL:: ASSUME ALLKNOW(atleast); l-ALLKNOW(atleast) FOL:: EVAL DEMO(ownCl.wltitel); 2--iDEMO(ownCl,whitel)Первый мудрец пытается доказать whitel в своём ownCl, но терпит неудачу. Второй мудрец слышит ответ первого и пытается попять, почему он не мог дать определенного ответа . FOL:': SWITCHCONTEXT meta2; FOL:: ASSUME ALLKNOW(atleast);- ALLKNOW(atleast) FOL::ASSUMEANSWERS(Sl,whitel,dontknow);- ANSWERS(Sl,whitel,dontknow)FOL:: EVALDEMO(addfact(black23,C21),whitel);- DEMO(addfact(black23,C21),whitel) FOL:: EVALACCEP1VIEW(Sl,black23);- ACCEPTVIEW(Sl,black23)

В этот момент нужно выполнить следующие шаги. Во-первых, необходимо обозначить аксиому рассуждения об ответе, в данном случае all-reason 1 для второго агента, идентичную соответствующей аксиоме для А , обозначенной посредством C21,atleast,whitel, и maknot(black23). Во-вторых, построить конъюнкцию появляющихся фактов, в данном случае конъюнкцию строк 1,2,3,4. В-третьих, применить к упомянутым двум формулам правило модус поненс. Одни и те же шаги повторяются несколько раз. Благодаря модус поненс, примененному к аксиоме all-reasonl, обозначенной с помощью С21, atleast, whitel и maknot(black23), получаем:5          - HOLDS(mknot(black23),C21)В этом месте можно было бы обновить С21. Но это не несет новой информации, поскольку white3 уже имеется в С21 в результате того, что А2, знает, что А1 знает цвет колпака А3 .Второй мудрец пытается теперь доказать white2 на основе собственных знаний. FOL:: EVAL DEMO(ownC2,white2);6          - ->DEMO(ownC2,white2)Не располагая достаточными знаниями для доказательства white2, второй мудрец вынужден ответить: "Я не знаю". Третий мудрец, услышав ответ второй начинает строить свое рассуждение. FOL:: SWITCHCONTEXT meta3; FOL:: ASSUMEALLKNOW(atleast);- ALLKNOW(atleast) FOL:: ASSUMEANSWERS(Sl,whitel,dontknow);- ANSWERS(Sl,whitel,dontknow) FOL:: ASSUMEANSWERS(S2,white2,dontknow);- ANSWERS(S2,white2,dontknow)Третий мудрец, прежде чем анализировать ответ второго, должен обновить свое представление о знаниях второго мудреца. С помощью правила модус поненс, примененного к аксиоме all-reasonl, обозначенной с помощью С32, atleast, whitel mknot(black23), получаем:0                    - HOLDS(mknot(black23),C32)FOL:: LET C32 = updatectx(C32,mknot(black23))BY{update};После обновления С32 третий мудрец может рассуждать об ответе, данном вторым. Используя правило модус поненс, примененное к аксиоме reason2, обозначенной с помощью white2 и mknot(mknot(white3)), получаем:- KNOWS(S2,mknot(mknot(white3))) FOL:: EVAL DEMO(C32,mknot(mknot(mknot(wltite3))))- -DEMO(C32,mknot(mknot(mknot(whUe3))))Правило модус поненс, примененное к аксиоме knows2, обозначенной с помощью mknot(mknot(white3)), приводит к:8- HOLDS(mknot(mknot(white3)),C32) FOL:: LET C32 = updatectx(C32,mknot(mknot(wliite3)))BY{update}; FOL:: EVAL DEMO(ownC3,mknot(mknot(mknot(white3))))- -iDEMO(ownC3,mknot(mknot(mknot(white3))))Правило модус поненс, примененное к аксиоме confidence2, обозначенной с помощью mknot(mknot(white3)), приводит к:1                    - HOLDS(mbiot(mknot(white3)),ownC3)FOL:: LET ownC3 = updatectx(ownC3,mknot(mknot(wlute3)))BY{update};После этого попытка третьего мудреца ответить на вопрос короля увенчалась успехом.FOL:: EVALDEMO(ownC3,white3); 10 - DEMO(ownC3,white3)Список литературы:Aiello L., "Automatic Generation of Semantic Attachments", Proc. of AAAI 80 (1980), pp. 90-93.Aiello L, Cecchi C, Sartini D., "Representation and Use of Metaknowledge", Proceedings of the IEEE, 74:10 (1986), pp. 1304-1321. -Aiello L, Levi G., "The Uses of Metaknowledge in AI Systems", Proc. of ECAI 84, O'Shea T. (Ed), North Holland (1984), pp. 705-717.Aiello L, Nardi D., Schaerf M., "Yet another soliution to the three wisemen puzzle", Proc. of ISMIS 88, Ras Z.Saitta L.(Eds.), (1988), pp. 398-407.Aiello L.,Nardi D.,Schaerf M., "Reasoning about Knowledge and Ignorance", to appear in Proc. of FGCS 88(1988).Attardi G.,Simi M., "Reasoning across viewpoints", Proc. of ECAI 84, O'Shea T. (Ed.).North Holland(1984), pp. 315-325.Batali J., "Computational Introspection", МГТ AI Memo 701 (1983).Bowen K.A., Kowalski R.A., "Amalgamating Language and Metalanguage", in Logic Programming, Tarnlund(Ed.), Academic Press, New York (1982), pp. 153-173.Coscia P., Franceschi P., Levi G., Sardu G., Torre L, "Object level reflection of inference rules by partial evaluation",in[24], pp. 313-327.
des Rivieres J., Levesque H.J., "The consistency of syntactical treatments of knowledge", Proc. of the 1986 Conference on Theoretical Aspects on Reasoning about Knowledge, in Halpern J. (Ed.), Morgan Kaufman, (1986), pp. 115-130.Farinas del Cerro, L., "MOLOG: a system for modal logics",New Generation Computing,(1986).Feferman S., "Transfinite Recursive Progressions of Axiomatic Theories", Journal of Symbolic Logic, 27:3 (1962), pp. 259-316.Geissler C, Konolige K., "A resolution method for quantified modal logics of knowledge and belief", Proc.of the 1986 Conference on Theoretical Aspects on Reasoning about Knowledge, in Halpern J.(Ed.),Morgan Kaufman, (1986), pp. 309-324.Genesereth M.R., "An Overview of Meta-level Architectures", Proc. of AAAI 83 (1983), pp. 119-124.Genesereth M.R., Nilsson N., "Fundamentals of Artificial Intelligence", Morgan Kaufman (1987).Giunchiglia F.Weyhrauch R.W., "A Multi-Context Monotonic Axiomatization of Inessential Non-Monotonicity", in [24] (1988), pp. 271-285.Hayes P.J., "In Defense of Logic", Proc. of IJCAI77 (1977), pp. 559-565.Hintikka J., "Knowledge and belief* Cornell University Press,Ithaca,New York,1962.Konolige K., "Circumscriptive Ignorance", Proc. of AAAI 82 (1982), pp. 202-204.Konolige K., "Belief and Incompleteness", in Hobbs J., Moore R.C. (eds.) Formal Theories of the Commonsense World, Ablex Pub. Corp., (1985), pp. 358403.Konolige K., "A Deduction Model of Belief", Morgan Kaufman Pub., (1986).Kripke S.A., "Semantical Considerations on Modal Logic", Acta Philosophica Fennica, 16, (1963), pp. 83-94.Lenzerini M.,Nardi D., "Belief revision as meta-reasoning", Proc. of ECAI 88 (1988), pp. 577-579.Maes P.,Nardi D.,(Eds.)Meta-levei Architectures and Reflection, North-Holland, 1988.Nait Abdallah M.A., "Logic Programming with ions", Proc. of the 14th Int. Coll. on Automata Languages and Programming,Otlmann T. (Ed.), LNCS 267, Springer Verlag (1987), pp. 11-20.Nardi D., "Evaluation and Reflection in FOL", in [24], (1988), pp. 195-207.Perlis D., "Languages with self-references I",Artificial Intelligence, 25, (1985), pp. 301-322.Perlis D., "Meta in logic", in [24], (1988), pp. 3749.Perlis D., "Languages with self-references H", Artificial Intelligence, 34, (1988), pp. 179-212.Simi M.Motta E., "OMEGA: an integrated reflective framework", in [24], (1988), pp. 209-226.Smith B.C., "Varieties of Self-Reference", Proc. of the 1986 Conference on Theoretical Aspects on Reasoning about Knowledge, in Halpern J. (Ed.), Morgan Kaufman, (1986), pp. 19-43.Weyhrauch R.W., "Prolegomena to a Theory of Mechanized Formal Reasoning", Artificial Intelligence, 13, 1 (1980), pp. 133-170.