Информационные логики тема автореферата и диссертации по математике, 01.01.06 ВАК РФ

V \ и ,.

.., и\'А

7 и ^ ^

С;

о

САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ

На правах рукописи УДС 519.49

Архангельскими Дкитрий Авенирович

ИНФОРМАЦИОННА ЛОГИКИ

01.01.06 - тематическая логика, алгебра и теория чисад

Автореферат диссертации ка соискание ученой степени кандидата физико-математических наук

Санкт-Петербург - 1993

Работа выполнена на кафедре алгоритмических языков и системного программирования Тверского государственного университета.

Научный руководитель - доктор физико-математических наук

профессор Тайцлин Михаил Абрамович.

Официальны? оппоненты - доктор физико-математических наук

Оревков В. П. (ЛОМИ), кандидат физико-математических наук Валиев Марс Кутдусович (Институт системных исследований.Москва;.

Ведувдяя организация - Московский государственный

унииверситет им. Ломоносова

Защита состоится "ОЬ" 40 1993 г. в часов назаседании специализированного совета К. 063.57.45 по присуждению ученой степени кандидата физико-математических наук вСакг-Петербургском Государственном университете (адрес совета 138904, Сакт-Петербург. Ст.Петергоф, Библиотечная' пл., 2, математюсо-мехакическия факультет СПбу;.

Защита будет проходить по адресу 191011, Сакг-Петербург, наб. реки Фонтанки, 27, 3-Я этаж, зал 311 (помещение ЛОМИ^.

С диссертацией можно, ознакомиться в Библиотеке им. А. М.Горького Санкт-Петербургского государственного университета. Университетская наб., 7^9.

Автореферат разослан " 0& 1993 г.

Ученый секретарь специализированного совета

Р. А.Шмидт

. ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ 1. Актуальность темы.

Понятие информационной логики было введено Павлаком. Информационны} логики можно рассматривать. как логики, отличающиеся от классических пропозициональных логик тем, что в них исследуются не умозаключения, а свойства некоторых объектов. Объекты представляются объединенными в некоторые совокупности, и нас .интересуют не только свойства отдельных объектов, но и различные, отношения, связыващие эти объекта Для описания отношений невду объектами используются модальности. В перзых .двух главах исследуются логики, описывающие статические свойства объектов. Формальная логическая система . описывает здесь совокупность объектов и связыващие их отношения. Идеология таких систем, названных Павлаком информационными, перекликается с идеологией . реляционных баз данных. База данных и базы знаний предназначены для хранения некоторой информации об изучаемых объектах. Однако доступная нам информация часто бывает неполной, особенно в таких областях информатики, как экспертные системы, представление знаний, распознавание образов- Как правило, мы не имеем полной информации, чтобы различать индивидуальныз объекты-мы можем лишь охарактеризовать эти объекты, посредством некоторых известных нам свойств- Языки информационных логик позволяют оперировать с информационными системами, не имеющими четкой информации об отдельных объектах- В третьей главе исследуются системы, в которых подобно тому, как это делается в объектно-ориентированном программировании, с каждым объектом связаны не только некоторые данныэ, но и средства преобразования этих данных, формальная логическая система, связанная с конкретным объектом, предназначена описывать возможные преобразования данных на . данном объекте в данном окружении. Для этого используются исчисления линейных логик,, базирующиеся на линейных логиках Жирара.

Первая глава данной работы связана с работами Евы Орловской и фаринаса Дел Церро, в которых предложен язык для описания данных к описана его семантика. При данном подхода данкыэ являются множеством объектов с установленными на них отношениями эквивалентности. Каэдое отношение эквивалентности описывает Некоторое свойство данных объектов. Каждое такое свойство разбивает множество объектов на непересекающиеся классы, подобно тому, как, например, в языках программирования, использующих

± -

разнообразны? дашсыз с различными свойствами, данныэ могут бЫ1Ь разделены по системе счисления на десятичные и двоичные и по способу представления на данныз с фиксированной и с плавающей точкой и т.п. К сожалению, цели, поставлешше авторами, не были достигнуты полностью, так как некоторые выводимые в предложенной формальной системе формулы не являлись тождественно истинными. В данной работе строится новая формальная система и доказывается ее корректность и полнота относительно, данной семантики, а также доказывается разрешимость построенной теории.

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

В третей главе продолжается изучение линейных логик Жирара, начатое Жираром в и развитое Абрамским Лафонтом. Линкольном, Митчеллом, Скердовым и Шанкаром. и Каноничен-

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

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

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

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

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

Научная новизна. Все основньв результаты диссертации является новыми.

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

Цель работы. Построить непротиворечивое полное исчисление для логики, описанной Орловской и Дал Цорро, решит сформулированный выше вопрос Вакарелова, исследовать линейныз логики с фиксированными ресурсами.

Апробация работы. Основньв результаты диссертации бьши доложены на 9 Всесоюзной конференции по математической логике в Ленинграде в 1988г., на международной конференции ьав'вэ в 1909 г,, на 10 Всесоюзной конференции по математической логике в Алма-ате в 1390 г., на международной шфренции исз'оз в 1992 г., на 11 Межреспубликанской конференции по математической логика в Казани в 1392 г. Они неоднократно обсуждались на заседаниях семинара по математической логики кафедры алгоритмических язьвсов и систомного

программирования Тверского государственного университета.

Структура и объем диссертации. Диссертация изложена на 107 страницах и состоит из введения и трех глав. Библиография содержит 22 названия.

РЕЗУЛЬТАТЫ ДИССЕРТАЦИИ

В первой главе даются некоторые определения.

Формулы логики dal строятся из следующих СИМВОЛОВ: пропозициональные переменные; реляционное переменные; -

классиические пропозициональные операции; - бинарные операции объединения и пересечения отношений соответственно; t з - унарная модальная пропозициональная бперация; - скобки. Каждое из множетв VAR пропозициональных переменных и и* реляционных переменных предполагается счетным.

Множество tRSL термов определяется как наименьшее множество, удовлетворяйте следующим условиям-. если x*rel,' то x«erö.; ¡¡у

если x.y*EREL, ТО С*иуЭ,СхПуЭ « EREL. МНОЖбСТВО ГОЯ форМУЛ ЯЗЫНЗ

dal определим как наименьшее, множество, удовлетворявшее следующим условиям! 1; если awar, то а*г<ж-, г), если то

-и. с лью, с и vb3, с л—»го « for,

Чтобы определить значения формул логики dal мы должны фиксировать некоторое множество ов объектов и некоторую решетку отношений эквивалентности на ов, соответствующих свойствам этих объектов. Под моделью мы понимаем тройку ®"сов, я.тз, где ов есть непустое множество,scово есть множество всех подмножеств множества ob.r есть некоторая решетка отношений эквивалентности, на ов.™ {varuepel) {s{ob)ur) есть, отображение, которое каждой пропозициональной переменной ставит в соответствие подмножество множества ов и каждому реляционному терму - отношение эквивалентности на ов, входящее в я. При этом ® ставит в соответствие терму *иу объединение отношений * и у в данной решетке а терму *">у - пересечение отношений * и у в данной решетке R.

Ниже объекты множества ов будут называться точками, а отображение « - отображением означивания.

Истинность формулы с з точке р модели я» С®-0 ь с) определяется следующими правилам» если c*var , то и, о ь с тогда и только ТОГДа, КОГДа о6«*СЭ;для СА&ю, САувз, са—ю истинность определяется стандартно, го.о > ixia тогда и только тогда, когда для любой точки о*«с® если С0.0^®"**3» то А-

Пусть - термы, « есть реляционная переменная, л.в ~

формула; выражение вида (си/хэ означает терм, полученный из терка . £ заменой каждого вхождения реляционной переменной « на вхождение терма *! выражение -вида лси/хз означает формулу, полученную из формулы а заменой каждого вхождения реляционной переменной « на вхождение терна *.

Теория г имеет следующие- схемы аксиом^ 1; все Сили достаточные для полноты; тавтологии классической пропозициональной логики,

2) Сх}СА-+Ю -* С1х]А —► С х]ВЗ, 7) и<11/хиуэ:м -» ИСи/хЭМ, 3} 1х}А —» а, . в; I ии/уих}1А иСи^хЭЗХ,

-СхЗ/4 СхЗ-ГхЗЛ, 9) £4С иУхЭЗА -* С 1Съ/хПу) ]А.

5) С IС и/хЗ ] А —¥ I 1СИУхих)1 А, Ю) С 1СмУх)1А —» С 4 С мУуПх) 3 А

6} С КгьОсЛхЭЗЛ —► [(Си/хЭ1А,

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

——р—^нодус поненс;. и; л С необходимость;. Мы будем обозначать тот факт, что ср.&етсх) через рх<?. Мы будем говорить, что тождество *<у вшолняется для термов х и у, если рх<? влечет ру<? для всех точек р и ? во всех моделях.

Теорема 1. Если формула гхз-ч-^узл доказуема в т для некоторой пропозициональной переменной то термы * и у удовлетворяют тожеству У*.

, Теорема 2. ■ Если выполняется тождество х<у, ю формула су1ч-.(х]<< доказуема в т для кавдой формулы л.

Заметим, что в качестве непосредственных следствий теоремы 2 получается .некоторые хорошо известные теоремы теории решеток. Например, если решеточное неравенство истинно во всех конечных решетках эквивалентностей, то оно истинно во всех решетках. Можно даже ограничиться такими' конечными решетками эквивалентностей, каждый класс эквивалентности которых содержит не более двух элементов. Поэтому имеется алгоритм для проверки тождественной истинности решеточного неравенства.

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

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

В главе 2 дается ряд определения.

МЫ будем ГОЕОРИТЬ. ЧТО ЧеТВерКа ОВ,ЛТ,<УЛ1.а. I а*АТ>.«ю

есть ^-система. где= ов есть непустое множество объектов: лг есть множество атрибутов; для каждого а из лт множество ум.а есть множество значений атрибута ш есть такая тотальная функция из множества ов*лт во множество рсуа^ всех подмножеств множества

УА1.-и<УА1.а I а^ЛТУ» ЧТО *аСх,с&Я/А1.а ДЛЯ ЛЮбОГО х*ОВ И й<МГ.

Здесь и ниже мы обозначаем множество всех подмножеств множества * через «ю.

Следуя Орловской и Павлаку и Вакарелову. в каждой юг-системе ^ мы определим следущив бинарнъв отношения на множестве ов-. *=.у тогда и только тогда, когда с с шсх, «о =тс у, «о э, •х^У тогда И ТОЛЬКО тогда, когда СУа«ЛГЭСтСх,аЭС«Су,о05, х&^у тогда И ТОЛЬКО тогда, когда СУа«ЛГЭСтСх,сЭптСу,аЭ«<ГО, а также унарное отношение

х«сг тогда и только тогда, когда для каадого атрибута а множество тсх.оэ содержит не более одного элемента-

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

В кяз, в дополнение к г мы определим сяедуюцие дополнительныэ базовыз отношения:

х>ву тогда и только тогда, когда у«,.*.

хОву тогда И ТОЛЬКО тогда, когда С^И У€к> да Сх«С и уеоэ. Кроме того мы будем рассматривать все отношения, получаемые из основных посредством теоретико-множественных операций' -.<■>.и -дополнения, пересечения и объединения соответственно, за исключением отношений (для в некотором смысле содержащих

сс-<эгу»э:). при этом мы можем исключить отношение = из списка базовых, так как это отношение определяется термом с «г.* э.

В множество основных отношений совпадает с ^ и все без исключения термы из -«г* являются допустимыми. Но : в мы рассматриваем только те системы, которые удовлетворяют следующим условиям: л не превосходит к для каждой цели вида \<хх<- ■ а число различных точек у, таких что у<ы и для любой такой

что г<у, не превосходит где Vх».....х^.у.^ов. < есть

с<пс-«э. N .- заранее заданная константа-

Под т мы будем понимать одно из отношений <. >. <. >. о.

Пусть и = сов. г") - абстрактная реляционная система, в которой ов непусто, а каждому символу из г\ поставлено в соответствие отношение тоя же местности на ов, мы будем говорить, что и есть стандартная ^-структура, если она удовлетворяет

УСЛОВИЯМ S1-S23 ИЗ СПИСКа i CS1-S24 для

Алфавит обеих логик ilí и состоит из следующих симеолов--

символы из счетного множества "¿к пропозициональных переменных; а> v - классические пропозициональные операции; >. с, d - реляционные константы, множество которых обозначается через ks; и, п, - - реляцио1шые операции объединения, пересечения и дополнения; л - специальная пропозициональная константа; с з -символ модальной операции; с. э .- скобки.

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

Мы будем использовать следухвде сокращения»

для'("i4vsí» <я> ДЛЯ "C-R1. 3 для C<r\». z ДЛЯ <

для С«П->3, > для С>(1-<)| т. ДЛЯ <</>Сcfv-tO&t>По-ЗСd&-cD, Gt ДЛЯ

Г ДЛЯ <Du-D>Cm&^i5> G.^ ДЛЯ ССчм.^Э. Г.^ ДЛЯ

сг.а<г>и-о>с-с.&^и1;э, И. ДЛЯ СГ^^-Г^), £t ДЛЯ

С<»Ст&Н Э&ГКЛо'К<>>Ст&Я Э —»ЮЗ-*[ЮС<»Ст&Н Э —Е, ДЛЯ г » 1 1 »

С.&С<»Ст&Н. 38,CRno-KO>Cm&W. )-.ЮЗ-»(К]С<»Ст&Н Э-+ЙЭ.

V l+i 1*1 »

ДЛЯ — -vo, для _ "M.

Для каждого рассматриваемого реляционного терма к мы определим симметричный ему терм следущим образом <s=>. ds=d,

oS=o. RS3=K, С-Ю3 = С КПП® = СК®ПТ*5 . CRuT3s = CRV).

Через mcx> мы обозначим тот факт, что и ъ>~°у для любой такой точки у, что у<*. Через |<* » тсхэ>| мы обозначим число элементов множества » тсхэ>.

Пусть и=сов, г^) есть реляцио!шая система. Рассмотрим отображение означивания «». которое символу R из г4 ставит в соответствие отношение к" из rtü и каждой пропозициональной переменной из var ставит в соответствие некоторое подмножество множества ов, на котором эта переменная истинна- Продолжим « на все реляционные термы из «п. так. что терма;! -я. Rns. rus соответствуют дополнение отношения «nQ«;. пересечение отношений

и Ч^. объедшшние отношения и «Ч^ соответственно. Определим теперь отношение * * л собъект * удовлетворяет формуле лэ следующим образок-- •

если л*уля, то х ь л тогда и только тогда, когда хвтсдэ, х ► тогда и только тогда, когда истинность для ~А< (,л*в)

определяется стандартно, х 1> с и-4 тогда и только тогда, когда у * л для каждого такого у*ов, для которого выполняется -хю^у. '

Слисок 1

В утверждениях 51 -^г* к. г обозначают допустимые отношения, а в формулах л\-м.я.лг*. - реляциозоше термы, соответствуйте этим допустимым отношениям в я и -и термы к и г предполагается

т « <<, <

S3 S3

s4. SB

S8

эквивалентными

SI xSy —» xRy, xRy —f уRsx. (Q xRy,y=e—» xRe > 6} x-Ra.xRy —♦ yfc Xäx,

gD хГу.уГв —♦ хГг, 63 х-"Га,хГу —♦ уГг, ВЗ х-Га.уТя —> х--Гу. 33 xRnSy —♦ XRy, бJ xRy —* xRuSy.

57 a^xRuSy-»xRy ИЛИ xSy, 63 xRy,Ив x-Sy —» xRnSy, & xRy.He xRiV-Sy—»xRnSy

58 ив *с«ггиу.

50 НЭ x«cf,xDy —» y€<i, 65 x«d, xDy —> y«d. IP x«d,x-Dy —► yea,

.JO xed.x"1 Oy —+ yed.

51 О x-'Dy.y-'Da —♦ xDn. Sil аЭ х<у,у«сГ -+■ x«d,

63 хва.х-Dy —x-'iy. SI 2 ycx —» xcx.

>; d>; x.y.e - объекты.

S13 аэ x^d.'xery —♦ x<y, 63 x-"<y,x«d —♦ x-'o'y, ВЗ хСоЛ-Оу —► х«а. SI4 x«d,x>y —» не У«*У-SI Баз x«ef, у , xoy —»C =ПоО у ßjxjry.x^d.y^cf—♦ -чту. БЭ хСат<уЭу.х€в1—»y«d. SIB аз xay,x<z —* аоу, 63 y^oe.xoy —♦ x~-<z, £5 a->o>y,x<z х-чуу. S17 xRy —» CxDy ИЛИ х-ОуЗ S18xDy ИЛИ x->Dy—»xRy ИЛИ x"»Ry

SIB xcx —♦ Hg xC->onOy.

530 ЭЗ x€d,y«ct —».xPy, 63 xed,y«d —» xDy. gi xed.ytsdx-'Dy.

531 не xRy —* x->Ry, sea xRy —♦ не x-'Ry. S23 xRy, xSy —+ xRoSy.

sa-t a;xo<xt<...<xN_r>He хн_4<хм. б; |<x i тсхэ> i < n.

в) тСхЭ, x«y.x<35,yRe—►yCRncOs, Г} тСхЭ —» не xafx.

и "-г имеют следующие схемы аксиом, в которых л.в -формулы, к^ого. и используются обозначения, принятые в списке 1=

все С или достаточна для полноту) тавталогии классической

- и -

пропозициональной логики,

г) IR1CA——» CCR1 .

з; схемы, соответствующие свойствам si-sie из списка i си формулы t<lMCd&-cD, fN,JN. ДЛЯ KRSJ.

/¿.1 и ii-г имеют следующие правила вывода;

модус поненоср.^-трглЧ"606^®®00715^

Теорема 4. И полны в стандартных структурах-таким образом, fti и «.г полны для стандартных структур и. следовательно, в силу леммы 2 они полны для ^-систем-

В третей главе даются некоторые определения. Мы фиксируем конечное множество s. элементы s будут называться запасами. Множество as - наименьшее, удовлетворяющее следующим условиям- s с as; если л « as. тогда си « os. Мы фиксируем конечное множество р. Элементы р имеют вид сх п. где х и у есть списки запасов. Элементы р будут называться базисными конверторами. Элементы объединения sup множеств s и р будут называться базисными ресурсами. Мы обозначим sup через R и ссюир через Мы

обозначим множество всех, натуральных чисел через

Модель есть, конечное дерево, вершинами которого являются ■объекты. Каждый объект характеризуется отображением из R в Для г из R и для объекта « выражение ос гэ обозначает число копий ресурса г в точке

Если а и (i есть объекты и ft есть прямой потомок <*. тогда мы пишем Пусть fi<?<*. если ft есть <>. Пусть г?«*"« есть ft«r и г^а для некоторого объекта г.

Пусть есть * и nUl/i есть оо\< для о. Пусть acd-^A^d-A, для такого ft, что « есть прямой потонок ft-

Выражения языка строятся из символов следующих множеств: s - множество пропозициональных переменных, называемых запасами; ь - символ секвенции-. —» символ бинарной операции линейной импликации; о - символ модальной операции-, с . э -скобки.

Множество for формул ' есть наименьшее, удовлетворяйте следующим условиям: s = For; формулы из s имеют сложность о; единственная подформула формулы из s есть она сама; если л,в « го г то ' сав"} ,са—*ву,па я for-, сложность слга или С/4—»ю равна

compCAl+complCBl+l , -. сложность см рзвиз сотрсхэ, гдв сотрСЮ и

сотрет есть сложности ли®; подформулами савз или СЛ-+ВЭ являются они сами и все подформулы л и в; единственная подформула си есть см.

с аю будем называть линейной конъюнкцией << и в.

Множество списков ресурсов есть наименьшее,

удовлетворяйте следующим условиям: г с = если л,в

е то сдвэ « RLiet. Множество а^си! есть есть наименьшее,

удовлетворяющее следующим условиям-- ск е, если л-в «

□^¿ве, то саю е Множество • пи.есть наименьшее,

удовлетворяющее следующим условиям: аз с оюлв^р с спилен если

л,в « свхсаг, тогда саю « оы.(в«. множество .....л >-¿.¿«1

списков формул .....есть наименьшее, удовлетворяющее

следующим условиям: \ с <\.....лу-иаь.....л «

<л . .л у-нач если л'в е <а.....а то слю «

1 П 4 П

<а.....а у-list.

» п

Определение закончено.

Пусть в « <Ак.....Ar>-Lisl. евзел .:>, обозначает число

вхождений ^ в в. Если в есть <\.....ц 1в1саэ=1 для /=

1.....п тогда в будет называться конъюнкцией ...../о.

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

Мы предполагаем, что любые два различных базисных конвертора не являются эквивалентными.

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

Выражения вида а ь в, где л и в - формулы, называется секвенциями. Если л эквивалентна сив эквивалентна то секвенции л »- в и с ь с называется эквивалентными.

Фиксируем некоторую модель и некоторую точку « модели.

Мы определим понятие канонического вида сапелъ формулы л. Если сапс,о совпадает с л, то * называется канонической.

Если л <= то сапСуО всть а. сагхСАВ^ = СсапСА^сапСВИ;

сапСА—+ВЭ" СсапС/О—»сапСЮ} ; сапсс/с = С с аггС а'/О с стС Ы1ВЗ 3 ;

сапса1с-4—сс<тса\о—если сл—»вэ не а~эквивалентна базисному конвертору и сапСа^С А-*Ю-> есть СеалСуО—♦сопСВ«, если с а а-эквивалентна базисному конвертору.

Сеювенция вида л в. где л,в « <л .. .Aj-nst. л « asust или \ - каноническая и о-эквивалентна базиснону конвертору называется элементарной секвенцией.

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

AeORList выше- ПУСТЬ ссхвэ 3d=t АЛ D+t 03 D; [сл—*гозо= сизо+свзо, еСЛИ

с а-*ю не о-эквивалентна базисному конвертору; t с а-*ю з d = с с и—»юзо, если с-4—»к> о-эквивалентна си-»ю и cu—ио есть базисный конвертор.

Мы говорим, что формула А ножет бнгь непосредственно преобразована в формулу в, если существуют такие формулы с.о,г, что л эквивалентна сссосо-»озэ и в эквивалентна с со. Отсюда транзитивным замыканием получается понятие преобразования формулы.

Пусть A0<At.....Ап - такой список канонических формул, что

формула \ получена из А0 удаленней всех символов о и для

'•i.....«-i формула непосредственно преобразуется из

Пусть для i-1....."--i формула л эквивалентна cc^d.cd^c^jd,

эквивалентна eco. Пусть * есть множество всех < из

<i.....п> таких, что со-»о не эквивалентна базисному

• конвертору. ' ■"

Мы говорим, что эта последовательность *t.....формул есть

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

если существует такое — ,n-i>, что сд-+о не эквивалентна никакому базисному конвертору, то существует такое

<«<i.....что не эквивалентна базисному конвертору и

далее называется корневыч конвертором, для каждого _/«<i..... ,í-i> формула с. эквивалентна конъюнкции сссо.-^г.эсгзс'э, формула с

эквивалентна сс-с"э, для каждого j-t*i.....n-i формула с.

эквивалентна сст.э, и последовательности

ccv. £>. dcD. зэ.....ccv о 3cd -+е 33. CV Е 3

».♦i i*i 1+1 41 rv-i n-i n—i п-i n-i n-i

tfccc'o jco-♦£■ 33.. . . ,сссг d. 3c d. —»г. 33. ссге.з

1111 i-l l-l v-i v-l 1 V

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

Если с" пусто, мы. предполагаем, что с. есть v.. Посредством удаления всех символов □ в каждая подформула формулы отображается на подформулу формулы Различны? подформулы отображаются на различные подформулы. Пусть для <=i.....n-i формула £>) отображается на

Мы говорим, что последовательность Аа-Аг.....формул есть

допустимое в точке « преобразование л, в в, где в □-эквивалентна если последовательность • - есть квазидопустимое преобразование и выполняются следующие условия достаточности

ресурсов: м зо-с tó')d<oicd:> да каждого базисного ресурса ь и

j« .

I* i l t

-Г [О'Ш^'О+Ы Ю^'гХ Г aCo'Di-r С А Зо)0+ Г Г С О' 1PJD

. J i 1 , le

jei * j=o j so keij =o

для каждого ¿»о и для каждого запаса о. _

Если мы говорим, что преобразование допустимо. Секвенция ^ s истинна в точка «, если существует допустимое в точке о преобразование cancho вв.

Для каждой модели и каждого объекта a мы определим исчисление линейной логики г*. Правила вывода не зависят от объекта В правилах а,в,с,о обозначают формулы и каждая из e.f.g.h или пусто или обозначает формулу. Правила вывода

t А Н СЧО С h ССв-»К>Ю ■ ' „ _ Л V В Л ' . . _

1 -ела ь ссьгып-. если s . если л h в

л i- с вю - элементарная секвенция; и с > d эквивалентны-.

í> А Ь свп СГО h р „„„„ Г оt» r canC/O h сапСОЭ

2 tcARib—ai t- ibn- если с в—о не в ——гттг— . a-эквивалентна базисному конвертору; л н о ■

СВСВ—»ОЗ КО car А АЗ t- сапС Ш '

3 ев^а ь ia-*v>> если л и в являются _ А ь свга . о-эквивалентными. с и о о-эквивалентны. тттевгт

Г jr> к с

к св-*с) ке п-эквивалекгна а ¿^а £ ¿ •.

базисному конвертору; Q сл-*в> к сх-»ю

4 —сгегттнзт если эквивалентна

базисному конвертору и с о-эквивалентна и о a-эквивалентна в.

Аксиомы та.

Для каждой мы добавим копия аксиомы л н л. Пусть Р есть такой объект, что Тогда для каждой мы добавим

ЛС/о копий аксиомы ои\< ь л.

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

вершины, по одному из правил 1-е.

Теорема 5. Если секвенция имеет доказательство в ты, тогда она имеет доказательство, в котором в любом вхождении правила 1

Г Ь СВП G b CCB-»D5H3 -CFSb h Ub£>X>-

секвенция <з и ссв—>а>мэ эквивалентна аксиоме вида св—»dd к св—*dd или получена по правилу 9.

Дэказательство в называется каноническим, если правило Б в нем не используется, любое вхождение правила 1-4 не встречается перед любым вхождением правила 7 и 8. каждая формула, входящая в это доказательство, является канонической и в любом правиле 1 вторая посылка эквивалентна аксиоме или получена по правилу 9.

Теорема . 6. Если секвенция в у с имеет доказательство в та, тогда секвенция сапсю ь canco имеет каноническое доказательство. Если эта секвенция - элементарная, то новое доказательство такие не содержит правил 2.3,

■ Теорема 7. Каждая доказуемая в тй секвенция истинна в <».

Теорема 8. Каждая истинная в « секвенция доказуема в т^.

Далее ' в ■ диссертации приводится алгоритм построения доказательства. Если сложность конверторов ограничена некоторой константой сложность .которого равна *c(lr,<n". где с есть константа- и п есть суммарная длина описания модели и секвенции.

Автор благодарен Михаилу Абрамовичу Тайцлину за большую помощь в работе над диссертацией.

Работы автора по теме диссертации, ti J Д. А- Архангельский, М. А. Тайцлин- Об одной логике для описания данных " Тезисы докладов 9 Всесоюзной конференции ло математической логике, Ленинград, 1988.

С 21 D. Archangel sky, М. Taltslin. On a logic for data description s/ LAB'89, LNCS. 1089, V. 383. 2-11.

с 3i Д. А- Архангельский. Расширенные информациошшэ логики

Тезисы докладов ю Всесоюзной конференции по математической логике, Алма-ата, «во. 7. с4> Д. А.. Архангельский. Булево замкнутые информационные логики с неточно определенными объектами " Сборник трудов Тверского : университета, Тверь. íeao;' эз-аг.

t5l D. Archangel sky. М. Taitslin, Modal linear logic /V LFCS'02, LNCST, 1992, v.BHO, 1-8.

- СБ1.Д.А- Архангельский, M.A. Тайцлин. Новая линейная логика ^

Теэисы докладов и Межреспубликанской конференции по математической логике. Казань, 1992. е. 171 Д. А- Архангельский. Негационная информационная логика " Сборник трудов Тверского университета, Тверь, юе2. и-17.