WWW.DISSERS.RU

БЕСПЛАТНАЯ ЭЛЕКТРОННАЯ БИБЛИОТЕКА

   Добро пожаловать!


Pages:     | 1 |   ...   | 25 | 26 || 28 | 29 |

Киевский национальный университет им. Тараса Шевченко, Киев E-mail:forlav@mail.ru Мальцевские чтения 2009 Неклассические логики и теория доказательств Модели логических систем продукционного типа, основанные на решетках С. Д. Махортов Алгебраическая логика представляет эффективный аппарат для моделирования логических систем. Однако в силу универсальности она оказывается недостаточно полезной в решении ряда важных задач, связанных с широко применяемыми на практике системами продукционного типа. К задачам такого рода относятся вопросы об эквивалентности, эквивалентных преобразованиях, верификации продукционных и подобных им систем, которые рассматриваются в ряде работ и решаются частными методами.

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

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

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

Воронежский госуниверситет, Воронеж E-mail:sd@expert.vrn.ru Мальцевские чтения 2009 Неклассические логики и теория доказательств Глобально допустимые правила WCP логик.

В. В. Римацкий Говорим, что правило r глобально допустимо в логике L, если r допустимо во всех фининто аппроксимируемых логиках, расширяющих логику L. Набор правил вывода R называется базисом глобально допустимых правил логики L, если (i) каждое правило из R глобально допустимо в L; (ii) любое глобально допустимое в L правило выводится из R во всех финитно аппроксимируемых логиках, расширяющих L.

Говорим, что финитно аппроксимируемая логика L, расширяющая логику S4, имеет слабое свойство ко-накрытий, если для любого конечного корневого L-фрейма F и произвольной антицепи X сгустков из F, фрейм F1, полученный добавлением как корня одноэлементного рефлексивного ко-накрытия ко фрейму cR, также являR cX ется L-фреймом. Логики, обладающие этим свойством будем далее называть WCPлогиками.

Теорема. Правило вывода r допустимо во всех финитно аппроксимируемых WCPлогиках, расширяющих S4, тогда и только тогда, когда r допустимо во всех табличных WCP-логиках, расширяющих S4.

Для всех чисел n>1, 1 i, j n; n N, определим формулы:

i := pi ¬pj; An := i; An,1 := (pi ¬q) ;

j=i 1in 1in B := q ¬q.

Определим также последовательность правил вывода:

An,1 ¬(An B) p ¬p R1 := ; Rn := ; n =2, 3,....

p ¬p ¬An Теорема. Множество правил {Rn, n N}, образует базис правил вывода, допустимых во всех финитно аппроксимируемых WCP-логиках над S4.

Множество R правил вывода в языке логики L будем называть квазибазисом для допустимых в L правил вывода, если любое допустимое в логике L правило вывода выводится из данного набора правил R.

Теорема. Множество правил {Rn, n N}, образует квазибазис правил вывода, допустимых во всех финитно аппроксимируемых логиках, расширяющих S4.

Теорема. Проблема глобальной допустимости произвольного правила r в S(финитно аппроксимируемой логике L0, S4 L0) разрешима.

Сибирский Федеральный Университет, Красноярск E-mail:Gemmeny@rambler.ru Мальцевские чтения 2009 Неклассические логики и теория доказательств К вопросу непротиворечивости семантического вероятностного предсказания С. О. Смердов Сначала определим вероятность на множестве основных предложений в соответствии с [1] (как распределение на подмножествах класса моделей 1-ого порядка G).

Далее позволим литералам (не только атомам) участвовать в классических объектах логического программирования: правилах, фактах и запросах; здесь вероятности основных экземпляров правил определены как условные.

µ {C | для некоторой основной вероятность C определена};

L L µ µ µ (C) inf {µ (C) | суть основная подстановка и C }, где C.

L L Пусть (B) —множество актуальных фактов исследуемой модели 1-го порядка B. Отношение C1 C2 (“быть более общим”) между C1 = (A1 B1,..., Bn) и µ C2 = (A2 D1,..., Dm) в имеет место в том лишь случае, когда существует L такая подстановка, что {B1,..., Bn} {D1,..., Dm}, A1 = A2 и C1 не является µ вариантом C2. Правила из, которые нельзя обобщить без потери в величине L условной вероятности µ (·), называются µ-законами; образуемое ими множество обоµ значим. Для всякого основного литерала H в результате семантического µL предсказания мы получаем наилучший µ-закон, если семантическое µ-предсказание H определено (все необходимые определения являют собой естественное расширение представленных в [2]). Каждому наилучшему правилу C=A B1,..., Bn, использованному в предсказании некоторого H, сопоставим все такие основные экземпляры C, что {B1,..., Bn} (B), A =H и {B1,..., Bn} µ-совместно (набор литералов S назовём µ-совместным, если вероятностная мера моделей, на которых он реализуется, отлична от нуля); совокупность описанных C (пробегая по всем литералам H) µ,обозначим.

L Теорема 1. Пусть некоторый основной атом H µ-предсказывается основным µ,0 µ экземпляром Cpos правила C1 (Cpos = C1pos), в то время как L L его отрицание ¬H — с помощью Cneg (Cneg =C2neg). Тогда множество литералов посылок Cpos и Cneg не µ-совместно.

µ,B = B1... Bn A | A B1... Bn {A| (A ) (B)} L Теорема 2. Пусть множество (B) µ-совместно. Тогда минимальная теория, содержащая B, логически непротиворечива.

Список литературы [1] Halpern J.Y. An Analysis of First-Order Logics of Probability. Artificial Intelligence, 46 (1990), 311– 350.

[2] Vityaev E.E. The logic of prediction. Mathematical Logic in Asia, Proceedings of the 9th Asian Logic Conference (Novosibirsk, Russia), (S.S. Goncharov, R. Downey, H. Ono, editors), Singapore: World Scientific, 2006, pp. 263–276.

Институт математики СО РАН, Новосибирск E-mail:netid@ya.ru Мальцевские чтения 2009 Неклассические логики и теория доказательств Автоматическое распознавание проективного свойства Бета в позитивно аксиоматизируемых локально табличных расширениях минимальной логики П. А. Шрайнер Л. Л. Максимовой в [1] было доказано, что минимальная логика Йохансона J имеет в точности семь позитивно аксиоматизируемых расширений, обладающих проективным свойством Бета. Шесть из этих логик являются локально табличными. Получаем что для того, чтобы проверить, будет ли позитивная логика, полученная добавлением новой схемы аксиом к позитивному фрагменту минимальной логики J, локально табличной логикой с проективным свойством Бета, нам достаточно выяснить, будет ли она совпадать с одной из вышеупомянутых шести логик.

Введем обозначения: Zn = {1,... n} с естественным линейным порядком; Vn = I {0, 1,... n} где 0Rx для любого x и ¬xRy для 1 x, y n, x = y; WIn = Zmin(I,n) k={-1} где -1Rx для любого x; Yn = Vn {-1} где -1Rx для любого x.

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

Предложение. Пусть L = J+ + {A1,..., Ak}, A = A1... Ak, A не выводима в J+, формула A содержит n переменных, r — общее количество вхождений «» в A и I = max(1, r). Тогда L имеет PBP тогда и только тогда, когда имеет место одно из следующих условий:

(1) Формула A опровергается на Z1.

(2) Формула A истинна на Z1 и опровергается на Z2.

(3) Формула A истинна на Zn+1 и опровергается на V2.

(4) Формула A истинна на Z2 и опровергается на Z3 и V2.

(5) Формула A истинна на Vmin(2n и опровергается на Z3.

,I) (6) Формула A истинна на WIn и опровергается на Y2.

Автором создана программа, реализующие вышеописанный алгоритм проверки проективного свойства Бета в позитивно аксиоматизируемых локально табличных расширениях минимальной логики Йохансона J.

Работа поддержана грантом РФФИ (номер гранта 09-01-00090-а).

Список литературы [1] Максимова Л. Л. Неявная определимость и позитивные логики. Алгебра и логика, 42 (2003), N. 1, 65—93.

[2] Maksimova L. Complexity of some problems in positive and related calculi. Theoretical Computer Science, 303 (2003), 171—185.

Институт математики им. С.Л. Соболева СО РАН, Новосибирск E-mail:schr@ngs.ru Мальцевские чтения 2009 Неклассические логики и теория доказательств Временная логика линейных по времени шкал с аксиомой индукции В. Ф. Юн Модальная логика отличается большим разнообразием синтаксиса и семантики.

Этим можно объяснить широкое применение модальных и временных логик, например, в информационных технологиях, теории искусственного интеллекта, математической лингвистике, и к изучению геометрических структур. Предметом нашего исследования является полимодальная логика, связанная с линейными временными моделями с моментами времени, которые являются кластерами состояний. Более точно, в [1] рассматриваются фреймы C(i), R с линейно упорядоченными R-кластерами iN состояний C(i), и изучается логика таких фреймов в языке с временными модальными операторами +, - и слабыми модальностями +, -. При задании логики посредw w ством моделей важнейшими задачами являются выбор модального языка и проблема аксиоматизации данной логики.

Мы ввели дополнительное отношение R1 между элементами соседних кластеров и рассмотрели более широкий класс фреймов вида X, R, R1, которые назвали линейными по времени (S R)Ind-фреймами. Поскольку слабые модальности не являются нормальными, то задача аксиоматизации существенно усложняется. Нами доказано, что если добавить к языку временные модальности +, -, то слабые модальности 1 + и - выражаются через другие. Поэтому при аксиоматизации класса линейных w w по времени (S R)Ind-фреймов естественно выбрать временной язык с четырьмя модальностями +, - и +, -.

1 В этом языке построено исчисление, содержащее аксиому индукции, полное относительно линейных по времени (S R)Ind-фреймов. Доказано, что оно финитно аппроксимируемо и, следовательно, является разрешимым.

Работа выполнена при финансовой поддержке Российского фонда фундаментальных исследований (проект 09-01-00090-а) и при поддержке гранта АВЦП Минобразования России «Развитие научного потенциала высшей школы» (проект 2.1.1/419).

Список литературы [1] Rybakov V. Discrete linear temporal logic with current time point clusters, deciding algorithms. Logic Log. Philos., 17 (2008), N. 1–2, 143–161.

Институт математики им. С. Л. Соболева СО РАН, Новосибирск E-mail:vetav@mail.ru Мальцевские чтения 2009 Неклассические логики и теория доказательств Новые константы в логике Даммета А. Д. Яшин Пусть Fm — множество формул пропозиционального языка со стандартными связками,,, ¬ и константами 0 и 1. Суперинтуиционистской логикой называется произвольное подмножество L Fm, включающее интуиционистскую пропозициональную логику Int и замкнутое относительно правил modus ponens и подстановки.

Например, логикой Даммета называется суперинтуиционистская логика, полученная добавлением к Int схемы аксиом (A B) (B A). Характеристическим для логики Даммета является, в частности, класс конечных линейно упорядоченных шкал (цепей).

Добавим к пропозициональному языку конечный набор = {1,..., n} логических констант. Расширенный класс формул обозначим через Fm(). Формулы из Fm называются чистыми.

-Логикой называется множество L формул расширенного языка, включающее Int и замкнутое относительно правил modus ponens и подстановки. -Логика L называется консервативным расширением логики L, если L Lи для всякой чистой формулы A из A L следует A L. -Логика L называется полным по П.С. Новикову расширением логики L, если L консервативна над L и для любой формулы A Fm(), не принадлежащей L, -логика L + A неконсервативна над L. Под проблемой Новикова для L понимается описание класса всех полных расширений данной суперинтуиционистской логики в конкретном расширении языка, в рассматриваемом случае с новым набором логических констант.

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

Теорема. Семейство полных по Новикову расширений логики Даммета в языке с новыми константами конечно и находится во взаимно однозначном соответствии с множеством попарно неизоморфных наростов.

Для описания наростов используется понятие универсальной -шкалы. Например, для двух дополнительных констант она состоит из 4-х компонент и выглядит так:

1 2 1 Московский городской психолого-педагогический университет, Москва E-mail:yashinaleksandr@list.ru Мальцевские чтения 2009 Неклассические логики и теория доказательств Temporal logics based on Kripke structures with embedded local frames S. Babenyshev, V. Rybakov We introduce a method for studying propositional logics, that are semantically generated by temporal (with future and past modalities) Kripke structures with embedded local frames.

The embedded frames have their own Kripke relations, possibly quite different from that of the parent temporal frame. The only restraining condition is that every embedded frame must reside inside a temporal cluster. We show, that whenever original Kripke structures satisfy constraints of certain modal logics, then the resulting logic retains the effective finite model property and decidability of the constituents. Furthermore, this method allows to add to the language some additional operations (not necessarily Kripke modalities), able to express higher-level properties of the underlying models, while still preserving the decidability of the resulting logic. This paper capitalizes on the previous research of one of the authors [1–5]. The generalization obtained has required a significant technical refining of the original approach.

This research is supported by Engineering and Physical Sciences Research Council, U.K.

(EP/F014406/1).

References [1] Rybakov V. In: Linear Temporal Logic with Until and Before on Integer Numbers, Deciding Algorithms. Volume 3967 of Lecture Notes in Computer Science. Springer, 2006, 322–334.

[2] Rybakov V. Logical consecutions in discrete linear temporal logic. Journal of Symbolic Logic, 70(4) (2005), 1137–1149.

[3] Rybakov V. Logical consecutions in intransitive temporal linear logic of finite intervals. Journal of Logic Computation, 15(5) (2005), 633–657.

[4] Rybakov V. Since-until temporal logic based on parallel time with common past. In: Logical Foundation of Computer Science. Volume 4514 of Lecture Notes in Computer Science. Springer, New York, USA, 2007, 486–497.

[5] Rybakov V. Logic of discovery in uncertain situations—deciding algorithms. In: KES 2007. Volume 4694 of LNAI., Vetri sul Mare, Italy, 2007, 950–968.

[6] Rybakov V. A criterion for admissibility of rules in the modal system S4 and the intuitionistic logic.

Algebra and Logica, 23(5) (1984), 369–384.

Institute of Mathematics, Siberian Federal University, 79 Svobodny Prospect, Krasnoyarsk, 660041, Russia E-mail:Sergey.Babenyshev@gmail.com Department of Computing and Mathematics, Manchester Metropolitan University, John Dalton Building, Chester Street, Manchester M1 5GD, U.K.

Pages:     | 1 |   ...   | 25 | 26 || 28 | 29 |






© 2011 www.dissers.ru - «Бесплатная электронная библиотека»

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