авторефераты диссертаций БЕСПЛАТНАЯ БИБЛИОТЕКА РОССИИ

КОНФЕРЕНЦИИ, КНИГИ, ПОСОБИЯ, НАУЧНЫЕ ИЗДАНИЯ

<< ГЛАВНАЯ
АГРОИНЖЕНЕРИЯ
АСТРОНОМИЯ
БЕЗОПАСНОСТЬ
БИОЛОГИЯ
ЗЕМЛЯ
ИНФОРМАТИКА
ИСКУССТВОВЕДЕНИЕ
ИСТОРИЯ
КУЛЬТУРОЛОГИЯ
МАШИНОСТРОЕНИЕ
МЕДИЦИНА
МЕТАЛЛУРГИЯ
МЕХАНИКА
ПЕДАГОГИКА
ПОЛИТИКА
ПРИБОРОСТРОЕНИЕ
ПРОДОВОЛЬСТВИЕ
ПСИХОЛОГИЯ
РАДИОТЕХНИКА
СЕЛЬСКОЕ ХОЗЯЙСТВО
СОЦИОЛОГИЯ
СТРОИТЕЛЬСТВО
ТЕХНИЧЕСКИЕ НАУКИ
ТРАНСПОРТ
ФАРМАЦЕВТИКА
ФИЗИКА
ФИЗИОЛОГИЯ
ФИЛОЛОГИЯ
ФИЛОСОФИЯ
ХИМИЯ
ЭКОНОМИКА
ЭЛЕКТРОТЕХНИКА
ЭНЕРГЕТИКА
ЮРИСПРУДЕНЦИЯ
ЯЗЫКОЗНАНИЕ
РАЗНОЕ
КОНТАКТЫ


Pages:     | 1 | 2 ||

«Томский политехнический университет На правах рукописи НОВОСЕЛЬЦЕВ Виталий Борисович ФОРМАЛЬНАЯ ТЕОРИЯ СТРУКТУРНЫХ ...»

-- [ Страница 3 ] --

Начиная с пустой секвенции путей, строим дерево вывода D из такое, что 1. D состоит только из -компактных секвенций путей;

2. образы формул всех верхних секвенций из D невыполнимы, пока не будет получено опровержение.

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

База индукции. Очевидно, что пустая секвенция является -компактом.

Индукционный шаг. Обозначим через Г образ формулы П.

Предполагаем, что Г невыполнима и не является аксиомой, а П – суть -компакт. Необходимо найти вывод с заключением П и посылками, удовлетворяющими подобным же свойствам. Если Г содержит только конъюнкцию или дизъюнкцию, то по лемме о -компактах существует ()-вывод, имеющий -компактные посылки и П в качестве заключения.

Поскольку ()-правила обратимы, то образы форму этих предпосылок также являются невыполнимыми. Если Г не содержит ни конъюнкцию ни дизъюнкцию и Г невыполнима, то имеется ()-вывод в KTФpath с заключением Г и невыполнимой предпосылкой Г. Несложно доказать, что в KTФpath существует ()-вывод с предпосылкой П такой, что Г является образом формулы П. По лемме о -компактах П является -компактом.

Завершение этого построения следует из того, что бесконечное построение дает бесконечное дерево вывода в KTФpath, которое существовать не может.

5.2. Полнота KTФIP без секвенций, относящихся к Выше рассматривалось доказательство теоремы полноты обратного метода с некоторыми критериями избыточности. Было построено исчисление KTФ,*IP, отличающееся от KTФIP тем, что в нем отсутствуют секвенции различной модальной длины и противоречивые пары путей. Модифицируем исчисление KTФ,*IP с учетом критерия избыточности для Ф-упорядочения.

Определение 5.8. Обозначим через KTФ, исчисление, полученное из KTФIP:

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

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

удалением всех выводов, не относящихся к.

В исчислении KTФ, справедливы лемма бимоделирования и лемма IP подсеквенциальности. Подобно случаю с немодифицированным исчислением обратных путей, для доказательства теоремы полноты обратного метода для KTФ, мы будем опираться на эти леммы.

IP Лемма (бимоделирования для KTФ, IP) 1. Пусть D – дерево вывода в KTФ, IP. Тогда образ формул D является деревом вывода Ф в KTФpath ;

2. Пусть D – дерево вывода секвенции А1,…,Аn в KTФpath и 1,…,n – такие пути, что Ф|i =Ai, i =1,…,n. Тогда существует дерево вывода D для 1,…,n в KTФpath такое, что D является образом формул дерева вывода D.

3. Пункты 1 и 2 справедливы, если везде «дерево вывода» заменить на «опровержение».

Доказательство леммы аналогично доказательству леммы бимоделирования для KTФpath.

Перед тем как перейти к лемме подсеквенциальности для KTФ, IP заметим, что исчисление KTФIP имеет различные правила для обработки конъюнкции. Поэтому мы изменяем определение дерева вывода, относящегося к Ф-упорядочению следующим образом.

KTФIP Определение 5.9. Дерево вывода в называется относящимся к Ф-упорядочению, если на вывод наложены следующие условия:

1) для каждого ()-вывода этого дерева Г, l, r() Г,, только, если l Г и r Г;

2) аналогично, для каждого (l)-вывода (соответственно (r)-вывода) этого дерева Г, l (l) Г, r (r) соответственно Г, Г, только если l Г (соответственно r Г);

3) и, аналогично, для каждого (r)-вывода этого дерева Г, r (r) Г, только если r Г.

Лемма (подсеквенциальности для KTФ, Пусть D – опровержение в KTФIP, IP).

относящееся к и в D существует вывод I:

Г1 … Гn, Г и пусть даны секвенции путей 1,…,n такие, что каждая i есть подсеквенция Гi. Тогда существует дерево вывода D для в KTФ, из 1,…,n такое, что IP является подсеквенцией Г.

Доказательство. Доказательство будем проводить, анализируя различные случаи для I.

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

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

Остается показать, как построить дерево вывода D так, чтобы оно относилось к. Проанализируем все возможные варианты выводов в KTФpath.

1. Пусть вывод I таков, что для его посылки Г, 1, 2, верно Ф|1=~ Ф|2.

Тогда 1,2 является подсеквенцией Г,1,2 и является аксиомой KTФIP.

Следовательно, мы можем взять в качестве D дерево вывода, состоящее из одной аксиомы 1,2. Очевидно, что такое дерево вывода относится к.

2. Пусть вывод I имеет вид:

П, l, r ();

П, Поскольку по условию леммы, l, r П, то D относиться к.

Мы предположили, что некоторая секвенция является подсеквенцией П, l, r и нашли дерево вывода в KTФ, IP подсеквенции П, из 1. Рассмотрим все возможные варианты:

1 не содержит ни l, ни r. В этом случае 1 является подсеквенцией П. Кроме того также является также подсеквенцией П, и пустое дерево вывода 1 из 1 доказывает этот случай.

1 содержит l и не содержит r. В этом случае 1=, l для некоторой подсеквенции из П. Следующее дерево вывода доказывает этот случай:

, l (l);

, l, r П Поскольку и секвенция является мультиподмножеством П, то справедливо, что l. Условие упорядочения можно проверить подобным способом для всех остальных правил вывода.

1 не содержит l, но содержит r. Этот случай симметричен предыдущему.

1 содержит l и содержит r. В этом случае 1=, l, r для некоторого мультиподмножества для секвенции П. Не умаляя общности, можно предположить, что l r (а отсюда следует, l, r).

что и Ниже приводится дерево вывода, доказывающее этот случай:

, l, r (l);

,, r (r);

,, (C);

, 3. Пусть вывод I имеет вид:

П, l П, r () П, Поскольку, по условию леммы l, r П, то D относиться к.

1, Предположим, что некоторые секвенции являются подсеквенциями, соответственно секвенций П, l и П, r, и, исходя из этих предположений, найдем дерево вывода в KTФ, подсеквенции IP П, из 1, 2.

Вновь рассмотрим все возможные варианты:

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

пусть секвенция 2 не содержит l. Этот случай симметричен предыдущему и доказывается аналогично.

пусть секвенция 1 содержит l и секвенция 2 содержит r. В 1 = 1, l 2 = 2, r этом случае и для некоторых мультиподмножеств 1 и 2 из П. Очевидно, что существует некоторая подсеквенцию П секвенции П, которую можно вывести из секвенции 1, 2, последовательно применяя правила вывода (С). Ниже приведено дерево вывода, которое доказывает этот случай:

1, l 2, r ();

1, 2, последовательность сокращений.

П, П 4. Пусть вывод имеет вид:

П, () Г, П, Допустим, что некоторая секвенция является подсеквенцией П,.

Найдем дерево вывода в KTФ, подсеквенции П,. Заметим, что это IP дерево вывода, также будет являться и деревом вывода для подсеквенции этого заключения, то есть для Г, П,.

Рассмотрим все варианты:

пусть секвенция не содержит. В этом случае является подсквенцией П, следовательно, имеет вид:, для некоторой подсеквенции из П. Ниже приведено дерево вывода в KTФ, IP, доказывающее этот случай:

, (+), пусть секвенция содержит. В этом случае имеет вид, для некоторой подсеквенции из П. Ниже приведено дерево вывода в KTФ, IP, которое доказывает этот случай:

, (), 5. Пусть вывод имеет вид:

П, () П, Предположим, что некоторая секвенция является подсеквенцией П,. Найдем дерево вывода в KTФ, подсеквенции П,.

IP Рассмотрим все возможные варианты:

пусть секвенция не содержит путь. В этом случае является подсеквенцией П, следовательно имеет вид: для некоторой подсеквенции из П. Ниже приведено дерево вывода в KTФ, IP, которое доказывает этот случай:

(+), пусть секвенция содержит путь. В этом случае имеет вид,, для некоторой подсеквенции из П. Ниже приведено дерево вывода в KTФ, IP, которое доказывает этот случай:

, (), Доказательство леммы завершено полностью.

Лемма подсеквенциальности легко обобщается до произвольного дерева вывода. Для этого необходимо применить метод математической индукции по длине дерева вывода. Сформулируем эту лемму без доказательства.

Лемма (подсеквенциальности для деревьев вывода в KTФ, IP). Пусть D – опровержение в KTФ, IP, которое относится к, D – поддерево вывода в D секвенции Г из секвенций Г1,…,Гn и 1,…, n – подсеквенции Г1,…,Гn соответственно. Тогда существует дерево вывода D для секвенции в KTФ, IP из 1,…, n такое, что является подсеквенцией Г.

Теорема 5.1. (полноты KTФ, IP) Формула Ф системы КТ невыполнима тогда и только тогда, когда имеет опровержение в исчислении KTФ, IP.

Доказательство.

Предположим, что формула Ф невыполнима. По теореме полноты для KTФpath секвенция имеет опровержение в KT Фpath. По лемме подсеквенциальности для деревьев вывода в KTФ, IP, существует подсеквенция секвенции, имеющая опровержение в KTФ, IP. Очевидно, что сама пустая секвенция имеет опровержения в KTФIP, поэтому она имеет опровержение и в KTФ, IP.

Предположим, что имеет опровержение в KTФ, IP. По лемме бимоделирования для KTФIP, формула Ф имеет опровержение в KTФinv.

Поскольку в KTФinv каждая секвенция, имеющая опровержение является невыполнимой, следовательно Ф – невыполнима.

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

Введем строгое понятие предпосылки для прямого и обратного исчислений путей KTФpath и KTФIP.

Определение 5.10. Пусть П и П – секвенции путей и секвенция П является подсеквенцией П. В этом случае будем говорить, что П предпосылает секвенцию путей П.

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

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

В процессе формализации будут использоваться идеи, которые заключаются в следующем.

Правила вывода необходимо переформулировать таким образом, чтобы они работали на множествах дизъюнктов [Bachmair and Ganzinger, 2000].

Далее необходимо доказать наиболее общие свойства деревьев вывода на таких множествах для того, чтобы обеспечить полноту в стиле [Voronkov 2000]. Затем надо доказать, что система с предпосылкой удовлетворяет этим свойствам.

Как и ранее в работе, будем рассматривать выводы, состоящие из нуля и более посылок и одного заключения. Кроме этого, будем предполагать, что все посылки и заключение правил вывода принадлежат множеству выводимых объектов, или просто объектов. Такими объектами в нашей работе являются секвенции из КТseq или КТФinv и секвенции путей из KTФpath и KTФIP.

Дедуктивная система – совокупность правил вывода и аксиом системы.

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

Предположим, что L – некая дедуктивная система на объектах. Мы превратим её в дедуктивную систему {L} на множествах объектов. Такую систему в дальнейшем будем называть множественным исчислением, а правила вывода для нее строить следующим способом:

Возьмем любой вывод из L :

П1… Пn (*) П тогда для любого множества объектов S правилом вывода в {L} будет:

S{П1, …, Пn} S{П1, …, Пn, П} Содержательно, под значением {L} будем понимать следующее:

множества объектов формализуют пространства поиска, правило вывода, приведенное выше означает, что если П1,…,Пn уже доказаны (это значит, что они уже принадлежат пространству поиска), то тогда П можно прибавить к пространству поиска при условии что (*) является выводом из L. Для обозначения выводов из {L} в дальнейшем будем использовать знак и запись: S{П1, …, Пn} S{П1, …, Пn, П}. В некоторых случаях будем надписывать над знаком название правила вывода.

Определение 5.11. Первоначальное множество объектов из {L} будем называть множеством аксиом из L.

С дедуктивной системой L также связано множество, называемое целевыми объектами. Например, в исчисленьях путей KTФpath и KTФIP целевым объектом является пустая секвенция.

Определение 5.12. Деревом вывода во множественном исчислении {L} называется любая последовательность выводов S0 S1 S2 …, возможно, неограниченная, где S0 есть первоначальное множество объектов.

Определение 5.13. Будем говорить, что дерево вывода D в системе {L} успешно, если некоторое множество Si из дерева вывода D содержит целевой объект.

Определение 5.14. Будем говорить, что дерево вывода D в системе {L} неуспешно, если ни одно из множеств Si из дерева вывода D не содержит целевой объект.

Теперь можно приступить к описанию стратегии предпосылки, которая удаляет избыточные дизъюнкты из пространства поиска вывода. Эта стратегия формализуется как правило вывода во множественном исчислении {L}, которое можно записать следующим образом: S{П1, П2} S{ П1} – здесь объект П1 предпосылает объект П2.

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

Предположим, что некоторое правило вывода добавляет объект П в пространство поиска, а затем введенное выше правило вывода удаляет его. В этом случае возможно, что будет получено бесконечное неуспешное дерево вывода вида:

S S{П} S S{П} … даже в случае, если успешное дерево вывода существует. Такое дерево вывода назовем «несправедливым», подразумевая, что существуют выводы, которые возможно применить к S, но они никогда не были применены.

Строго формализуем понятие «справедливости».

Определение 5.15. Пусть D = S0 S1 S2 … – дерево вывода в системе {L}.

Множество i ji Sj назовем пределом дерева вывода D.

Очевидно, что предел состоит из секвенций, которые всегда остаются в дереве вывода после любого шага.

Определение 5.16. Пусть D = S0 S1 S2 … – дерево вывода в системе {L}.

Дерево вывода D называется справедливым, если для любого правила вывода из L, имеющего вид:

П1… Пn П где П1… Пn принадлежат пределу дерева D, вывод из {L}, имеющий вид:

S{П1, …, Пn} S{П1, …, Пn, П} применен в дереве вывода, иными словами, для некоторого i и S, множество Si имеет вид:

S{П1, …, Пn}, а множество Si+1 имеет вид:

S{П1, …, Пn, П}.

Ниже приведено доказательство теоремы полноты для исчисления {KTФ, IP}, которое является системой множественного вывода, полученной из KTФ, IP. Из доказательства этой теоремы станет ясно, что эта система является наиболее общей и применима к любой системе вывода без вычеркивающего правила.

Теорема 5.2. (полноты для {KTФ, IP}). Пусть Ф – формула КТ и есть Ф-упорядочение.

Тогда 1. если какое-либо дерево вывода в {KTФ, IP} успешно, тогда формула Ф невыполнима;

2. если формула Ф невыполнима, то любое справедливое дерево вывода в {KTФ, IP} успешно.

Доказательство.

1. Предположим, что дерево вывода S0 … Sn успешно. В этом случае любая секвенция ПiSi имеет опровержение в KTФ, IP. А следовательно, также имеет опровержение. По Теореме полноты для KTФ, можно IP сделать заключение, что формула Ф – невыполнима.

2. Предположим, что S = S0 S1 … – справедливое дерево вывода.

Докажем, что любая секвенция путей П, имеющая опровержение в KTФ, IP, встречается в некотором Si. Доказательство проведем индукцией по длине опровержения секвенции П. В случае, если опровержение нулевой длины, то есть секвенция П является аксиомой, она уже является элементом множества S0. Для доказательства опровержения длины, большей нуля, рассмотрим последний вывод этого опровержения:

П1… Пn П Согласно индукционной гипотезе, любая секвенция Пi входит в некоторое Sk i. Поскольку {KTФ, IP} не вычеркивает никакую секвенцию путей, то все секвенции Пi принадлежат пределу S. В таком случае, по определению справедливости S, секвенция П также будет являться членом некоторого множества Sm.

Перед тем как приступить к доказательству теоремы полноты для {KTФ, IP} с предпосылкой, определим более строго само понятие предпосылки. Затем покажем, что {KTФ, IP} является полным с этим более строгим понятием.

Определение 5.17. Будем говорить, что секвенция путей П.

префиксно-предпосылает секвенцию путей П, если для любого пути П П.

существует такой путь П П, что.

Заметим, что префиксная предпосылка является стандартным мультимножественным расширением понятия упорядочения (см., например, [Niwenhuis and Rubio 2000]).

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

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

{KTФ, Определение 5.18. Исчислением IP} с префиксной предпосылкой называется дедуктивная система, полученная из {KTФ, IP} добавлением следующего «правила префиксной предпосылки»:

S{П, П} S{П}, где П префиксно-предпосылает П и П П.

Отметим, что понятие справедливого дерева вывода, введенное выше, требует только того, чтобы выводы первоначального исчисления применялись за несколько шагов. Теперь мы имеем новые варианты поведения (разновидности шагов), которые позволяют вычеркивать избыточные секвенции из пространства поиска вывода. Будем использовать старое понятие справедливости для {KTФ, IP} с префиксной предпосылкой, то есть не станем требовать, чтобы правило префиксной предпосылки, применяемое к предельным секвенциям, выполнялось за несколько шагов.

Таким образом, любое справедливое дерево вывода в {KTФ, IP} с префиксной предпосылкой является также справедливым деревом вывода в {KTФ, IP} без префиксной предпосылки.

Сформулируем без доказательств некоторые достаточно очевидные свойства префиксной предпосылки, которые в дальнейшем будут использоваться при доказательстве теоремы полноты для {KTФ, IP} с префиксной предпосылкой.

Лемма 5.i. Пусть даны секвенции путей П и П. П предпосылает П тогда и.

только тогда, когда мультимножество П П пусто.

Лемма 5.ii. Пусть даны секвенции путей П и П. Если П предпосылает П, тогда П префиксно-предпосылает П.

Лемма 5.iii. Пусть даны секвенции путей П и П. Если П префиксно предпосылает П и П префиксно-предпосылает П, тогда П=П.

Лемма 5.iv. Пусть даны секвенции путей П, П и П. Если П префиксно-предпосылает П и П префиксно-предпосылает П, тогда П префиксно-предпосылает П.

Лемма 5.v. Пусть даны секвенции путей П, П и пути 1,…,n. Если 1, …, n и секвенция П префиксно-предпосылает П.

Лемма 5.vi. Пусть даны секвенции путей П, П и путь. Если и П, секвенция П префиксно-предпосылает секвенцию П, тогда префиксно-предпосылает П,.

Лемма 5.vii. Не существует бесконечной последовательности П0, П1, … такой, что П i+1 префиксно-предпосылает Пi и Пi+1 Пi.

Большинство этих лемм непосредственно следуют из стандартных фактов относительно мультимножественного расширения хорошо основанных порядков, подробные доказательства которых можно найти в [Niwenhuis and Rubio 2000]. Так, например, отношение префиксной предпосылки является хорошо основанным, поскольку таковым является.

После доказательства теоремы полноты для {KTФ, IP} с префиксной предпосылкой, мы отметим еще два дополнительных свойства, связанные с оптимизацией поиска доказательства.

Определение 5.19. Пусть П, П – секвенции путей, S – дерево вывода. Будем говорить, что секвенция П удаляется в S через П, если некоторое Si+1 = Si\{П} и секвенция ПSi+1 префиксно-предпосылает П.

Определение 5.20. Для любой секвенции путей П (она не обязана принадлежать множеству Si) следом П в S называется секвенция П S такая, что П префиксно-предпосылает П и не существует П S такой, что П префиксно-предпосылает П.

Теорема 5.3. (полноты для { KTФ, IP} с префиксной предпосылкой).

(1). Если любое дерево вывода в системе {KTФ, IP} с префиксной предпосылкой успешно, то формула Ф логики КТ невыполнима.

(2). Если формула Ф логики КТ невыполнима, то любое справедливое дерево вывода S в {KTФ, IP} с префиксной предпосылкой успешно.

Доказательство.

(i) Сначала покажем, что верно (2), точнее, что оно следует из условия (1). Пусть Т – справедливое дерево вывода в {KTФ, IP} и секвенция путей П встречается в Т. Тогда существует секвенция пути Г, префиксно-предпосылающая П и принадлежащая пределу S.

Предположим, что условие (1) теоремы справедливо и Ф – невыполнима, тогда по теореме полноты для {KTФ, IP} без предпосылки дерево вывода Т содержит секвенцию путей. Из этой же теоремы следует, что S должно содержать секвенцию путей, префиксно-предпосылающую. Но существует только одна такая секвенция путей – сама. Таким образом, если (1) справедливо, то справедливо и утверждение (2) теоремы.

Рассмотрим теперь словие (1) теоремы.

(ii) Пусть S S0 S1 …, обозначим через S предел S.

Если секвенция П удаляется через П1, то возможно что и секвенция П удаляется через П2 и так далее, но лемма 7 гарантирует, что такое построение нельзя продолжать бесконечно, поэтому, начиная с некоторого j, все множества Sj будут содержать совпадающие секвенции путей П, которые префиксно-предпосылают П. Этим доказано следующее утверждение:

(iii) Для любой секвенции путей П в любом множестве Si существует секвенция ПS такая, что П префиксно-предпосылает П.

Более того, используя аналогичные рассуждения, можно усилить этот результат до следующего утверждения:

(iv) Для любой секвенции путей П в любом множестве Si существует секвенция П S такая, что П префиксно-предпосылает П и, если П S префиксно-предпосылает П, то П = П.

Исходное (iii) можно переформулировать следующим образом:

(iii`) Любая секвенция путей ПSi имеет след в S.

Для доказательства (1), а следовательно, и всей теоремы, докажем еще более общее, нежели (iii), утверждение, из которого (1) непосредственно следует:

(v) Любая секвенция путей П, встречающаяся в справедливом дереве вывода Т в {KTФ, IP} имеет след в S.

Пусть Т = Т0 … Тi …. Возьмем наименьшее i такое, что П Тi.

Утверждение (v) будем доказывать индукцией по i.

Если i=0, то П – аксиома, следовательно она принадлежит S0, и по (iii) имеет след в S. Если i 0, тогда П получается выводом I в KTФ, из IP секвенций путей в Тi-1. По предположению индукции эти секвенции путей имеют следы в S. Проанализируем все возможные случаи на выводе I, но прежде отметим несколько важных общих свойств, связанных с избыточностями и префиксной предпосылкой. А именно, докажем следующие два утверждения.

(vi) Пусть П – секвенция путей, содержащая пару противоречивых путей 1, 2 и П префиксно-предпосылает П, тогда П также содержит пару противоречивых путей.

(vii) Пусть П и П префиксно-предпосылает П, тогда П.

Доказательство (vi) следует из того факта, что если 1, 2 П и П префиксно-предпосылает П, тогда существует 1, 2 П такие, что 1 1 и 2 2. Следовательно, если 1, 2 — противоречащая пара путей, то 1, 2 также являются противоречивой парой путей.

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

Вернемся к доказательству (vi) и разберем последовательно все правила вывода из KTФ, IP.

I. Вывод I имеет вид:

П, l (l);

П, Пусть Г – след П, l в S. Рассмотрим три возможных случая:

a) Г префиксно-предпосылает П. Тогда Г также префиксно-предпосылает П, и является следом П,.

b) Г имеет вид Г, l, где Г префиксно-предпосылает П. Рассмотрим вывод:

Г, l (l) Г, Покажем, что этот вывод не является избыточным в KTФ, IP.

Очевидно, что Г, не содержит пару путей различной модальной длины, так как таким же является Г, l. Утверждение (6) гарантирует, что Г, не содержит противоречивых пар путей, поскольку таковы П,, и, наконец, (7) гарантирует, что Г, поскольку П.

Поскольку вывод (п.b) не является избыточным, и дерево вывода S справедливо, то следовательно S содержит этот вывод. Согласно утверждению (3), дерево S содержит след Г,, очевидно, что этот след является также следом П,.

Теперь нам достаточно доказывать лишь то, что выводы в S неизбыточны.

Случай (c): Г имеет вид Г,, где Г префиксно-предпосылает П и c) l.

Заметим, что если, то Г, также префиксно-предпосылает П,. Поэтому можно ограничиться лишь случаем, когда =.

Используя определение префиксной предпосылки, можно показать, что Г, префиксно предпосылают П, в случае b) либо Г.

Покажем, что последнее невозможно. – Действительно, Г подразумевает, что Г, имеет вид Г,, для некоторого Г.

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

II. Вывод I имеет вид:

П, l П, r () П, Возьмем следы Г1 и Г2 для П1, l и П1, r, соответственно, в дереве вывода S. Подобно предыдущему случаю рассмотрим возможные варианты:

a) Г1 префиксно-предпосылает П1, либо Г2 префиксно-предпосылает П2. – Тогда либо Г1, либо Г2 префиксно-предпосылает П1, П2,.

Г1 содержит l и Г2 содержит r. Тогда Г1 имеет вид Г1, l и Г b) r имеет вид Г2, и они таковы, что Г1 и Г префиксно-предпосылают П1 и П2 соответственно. Поскольку дерево S справедливо, то оно содержит вывод:

Г1, l Г2, r () Г1, Г2, Согласно утверждению (3), дерево вывода S содержит след Г1, Г2,.

Очевидно, что этот след также является следом П1, П2,.

Г1 имеет вид Г1,, где Г1 префиксно-предпосылает П1 и c) l.

Этот случай подобен рассмотренному выше случаю с конъюнктивным выводом.

Г2 имеет вид Г2,, где Г2 префиксно-предпосылает П2 и d) r.

Этот случай доказывается аналогично предыдущему.

III. Вывод I имеет вид:

П, () П, Возьмем след Г от П,. Все пути в П, имеют одинаковую модальную длину, следовательно каждый собственный префикс любого пути в П, имеет модальную длину меньше, чем у. Это значит, что Г либо состоит только из путей в П,, либо из префиксов из П,. В последнем случае, используя тот факт, что Г является следом, можно доказать как и в случае (Iс), что Г префиксно-предпосылает П,. Итак, остается доказать случай, когда Г состоит из путей в П,. Заметим, что Г не может содержать копии, поскольку Г является следом.

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

Г не содержит. В этом случае Г является подсеквенцией П, a) следовательно Г имеет вид Г для подсеквенции Г из П.

Рассмотрим вывод:

Г (+) Г, Поскольку дерево вывода S является справедливым, то оно содержит этот вывод. Легко увидеть, что Г, предпосылает П, и таким образом также префиксно-предпосылает П,. Возьмем след Г, в дереве S. Очевидно, что он также является следом для секвенции П,.

Г содержит. В этом случае Г имеет вид Г, для некоторой b) подсеквенции Г из П. Рассмотрим следующий вывод:

Г, () Г, Поскольку дерево вывода S справедливо, то оно содержит этот вывод. Легко заметить, что Г, предпосылает П, и таким образом также префиксно-предпосылает П,. Возьмем след Г, в S.

Очевидно, он также является следом для П,.

IV. Вывод I имеет вид:

П (+) П, Этот случай, практически, идентичен предыдущему.

V. Вывод I имеет вид:

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

Г не содержит. В этом случае Г является подсеквенцией П, a) следовательно Г имеет вид Г для подсеквенции Г из П.

Рассмотрим следующий вывод:

Г (+) Г, Поскольку дерево вывода S является справедливым, то оно содержит этот вывод. Легко увидеть, что Г, предпосылает П, и таким образом также префиксно-предпосылает П,. Возьмем след Г, в дереве S. Очевидно, что он также является следом для секвенции П,.

Г содержит. В этом случае Г имеет вид Г, для некоторой b) подсеквенции Г из П. Рассмотрим следующий вывод:

Г, () Г, Поскольку дерево вывода S справедливо, то оно содержит этот вывод. Легко заметить, что Г, предпосылает П, и таким образом также префиксно-предпосылает П,. Возьмем след Г, в S.

Очевидно, он также является следом для П,.

Доказанная теорема полноты для {KTФ, IP} с префиксной предпосылкой имеет несколько приложений (помимо возможности удаления предпосылающих секвенций из пространства поиска). Обсудим важное следствие.

Рассмотрим любой (*) вывод:

П, * (*) П, Заметим, что заключение этого вывода префиксно-предпосылает предпосылку. Таким образом, предпосылку можно отбросить, как только применено правило. Более того, это можно проделать даже когда * не является максимальным в П, *. – Следовательно, вывод избыточен. Если мы применяем (*)-правила энергичным способом (как только это возможно), то любой путь * становиться «недолгоживущим». Это наблюдение весьма существенно в практическом плане: можно модифицировать исчисление {KTФ, IP} так, чтобы такие пути вообще не встречались в секвенции.

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

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

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

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

Показана полнота теорий и сформулированы соответствующие алгоритмы.

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

Аспирантское исследование Д.С.Ларионова [Ларионов 2006] по применению разработанного подхода к автоэпистемической логике S5, начатое под руководством автора настоящей диссертации, успешно завершено с практической реализацией, что также подтверждает перспективность, мощь и универсальность рассмотренной методологии.

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

Выделенный в работе класс РДС-моделей обладает рядом привлекательных свойств:

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

2. Естественный порядок, определяемый структурой описания, позволяет осуществлять поиск решения задачи T=(A0,X0,S) локально на подсхемах, причём на каждом этапе – работе с одной подсхемой – используется информация, касающаяся только данной подсхемы. Это позволяет формировать пространство вывода только из прикладных аксиом (ФС), которые принадлежат вовлекаемым в вывод подсхемам.

3. Информация о работе на каждой подсхеме фиксируется и может использоваться в дальнейшем – обеспечивается бесповторность поиска решения («запроцедуривание»).

4. Ограничения на использование рекурсивных конструкций позволяют синтезировать алгоритмы, в которых на синтаксическом уровне предусмотрен выход из рекурсии. Завершаемость таких программ зависит только от задания семантики прикладной составляющей РДС-модели.

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

Описанная теория РДС-моделей может служить естественным формальным базисом популярного объектно-ориентированного подхода.

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

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

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

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

Диссертационное исследование определяет достаточное количество «точек роста» – новых направлений работы, которые могут оказаться полезными в областях распределенного управления, нейроинформатике, семантическом лингвистическом анализе, CASE-технологиях и так далее.

СПИСОК ПУБЛИКАЦИЙ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Новосельцев В.Б. Синтез рекурсивных программ в системе СПОРА Препринт – 43. Ленинград: ИТА АН СССР «Алгоритмы небесной механики», 1985. – 45 c.

2. Новосельцев В.Б. Структурные вычислительные модели // Труды Конференции «Синтез программ» / ЦНТИ. – М., 1985. – С. 17-23.

3. Новосельцев В.Б., Калайда В.Т. Концепции построения программного окружения для решения задач оптики атмосферы // Журнал оптики атмосферы. – 1986. – №6. – С. 43-51.

4. Новосельцев В.Б. Синтез рекурсивных программ без развертки модели // Межд. научно-техническая конференция «Прогр. обесп. ЭВМ. Калинин-87» / ГЦНТИ. – Калинин, 1987. – С. 54-59.

5. Zurenapel F., Novoseltsev V. Toward the automatic deductive proof of the recursive formula in special intuitional theories // Communications on Discrete Applied Systems. – 1990. – №3. – pp. 356-364.

6. Новосельцев В.Б. Некоторая формализация недетерминированных процессов // Международная конференция «Параллельные вычисления-1991» / ИК АН Украины. – Киев, 1991. – С. 37-41.

7. Новосельцев В.Б, Калайда В.Т., Шагисултанов В.Г. Разработка программного обеспечения для представления управляемых объектов в системах связи. Н/Т отчет // ИОА СО РАН. – № К5–14/91–Гб. – Томск, 1991. – 84 с.

8. Novoseltsev V. Automatic inference engine for structured model theory // Applicationes de Logique. – 1991. – № 2. – pp. 65-68.

9. Новосельцев В.Б., Бойцов С.Н. Иерархическая модель сложной динамической системы // Рукопись деп. ВИНИТИ. – 1996. – 28 c. – №1206-В1996.

10. Novoseltsev V. Computational models and recursive program synthesis // 5th International Symposium on Applied Logic / IK AS Estonia. – Tallinn, 1996. – pp.

76-82.

11. Новосельцев В.Б., Нам Ю.Б. Формализм для представления и анализа сложных информационных комплексов // III Сибирский Конгресс по прикладной и индустриальной математике / ТГУ. – Томск, 1998. – С. 25-30.

12. Новосельцев В.Б., Бурлуцкий В.В. Логический вывод в дедуктивных системах // Вторая сибирская школа молодого ученого / НГТУ. – Новосибирск, 2001. – С. 27-41.

13. Новосельцев В.Б., Бурлуцкий В.В. Подход к реализации вывода в различных льюисовских системах // Логика и приложения. – 2001. – С. 61-65.

14. Новосельцев В.Б., Бурлуцкий В.В. Реализация обратного метода для модальной логики KT // Исследования по анализу и алгебре / ТГУ. – Томск, 2001. – С. 54-60.

15. Новосельцев В.Б., Тютерев В.В. Метод динамического наращивания узлов как способ построения нейронных сетей эффективного размера // Нейрокомпьютеры: разработка и применение. – 2001. – №2. – С. 82-88.

16. Новосельцев В.Б., Тютерев В.В. Автоматическое построение нейронных сетей методом эволюционного наращивания // Рукопись деп. ВИНИТИ, ТГУ. – 2001, №1944-В2001. – 26 c.

17. Новосельцев В.Б., Ларионов Д.С. Оболочка экспертной системы на основе нечетких рассуждений с прямым и обратным выводом // Математическое моделирование, ИММ РАН: т.14.– 2002. – №9 – С. 48-52.

18. Новосельцев В.Б., Романчук Е.А. Нечеткие множества в когнитивных системах // Труды ИСП РАН: т. 7. – 2004. – С. 55-60.

19. Новосельцев В.Б., Соколова В.В. Расширение алгебры Кодда операциями с рекурсивными объектами // Вестник ТГУ. – 2004. – №284. – C. 54-59.

20. Новосельцев В.Б., Колтун П.Н., Романчук Е.А. Возможность использования дескрипторных логик в системе управления знаниями // Вестник ТГУ. – 2004.

– №284 – С. 17-22.

21. Novoseltsev V., Sokolova V. Expansion of Codd algebra by recursive definitions // Korea-Russia International Symposium on Science & Technology “KORUS 2004” / Tomsk, 2004. – pp. 54-57.

22. Новосельцев В.Б., Малахов А.В. К вопросу о синтезе параллельных алгоритмов // Вестник ТГУ.– 2004. – №284. – С. 35-39.

23. Новосельцев В.Б., Романчук Е.А. О манипулировании знаниями с использованием нечетких множеств // Оптика атмосферы и океана. – 2005. – №4. – С. 867-871.

24. Novoseltsev V. Theorem proving in normal modal system of KT-family // Proc. of 8th International Conference on Mathematics. – Spain, 2005. – pp. 82-88.

25. Новосельцев В.Б., Аксенов С.В. Организация и использование нейронных сетей. – Томск: НТЛ, 2006. – 160 с.

26. Новосельцев В.Б. Теория структурных функциональных моделей // Сибирский математический журнал. – 2006. – №5. Т. 47. – С. 1014-1030.

27. Новосельцев В.Б., Аксенов С.В. Повышение качества распознавания сцен нейронной сетью определенного вида // Известия Томского политехнического университета. – 2006. – №6. Т. 309. – С.150-160.

28. Новосельцев В.Б., Коваленко Д.А. Стратегия установления выводимости формул в структурных функциональных моделях // Известия Томского политехнического университета. – 2006. – №6. Т. 309. – С. 112-118.

29. Новосельцев В.Б., Копаница Г.Д. Нецелеориентированная стратегия вывода формул в модальных исчислениях // Известия Томского политехнического университета. – 2006. – №6. Т. 309. – С. 11-20.

30. Новосельцев В.Б., Соколова В.В. Обработка рекурсивных данных конечными автоматами // Известия Томского политехнического университета. – 2006. – №6. Т. 309. – С. 54-58.

Список цитируемой литературы Новиков и Петрушина (Бабаев И.О., Новиков Ф.А., Петрушина Т.И.) 1.Бабаев, [1981] Язык Декарт - входной язык системы СПОРА // Прикладная 1.1.

информатика, вып.1. – М.:«Финансы и статистика». 1981.

С.35-73.

и Новосельцев (Бабаев И.О., Новосельцев В.Б.) 2.Бабаев [1983] Синтез рекурсивной программы по описанию рекурсивного 2.1.

отношения в языке Декарт // Применение методов мат. логики.

Всес. конф. ИК АН ЭССР. – Таллин. – 1983.


(Барвайс Дж.) 3.Барвайс [1983] Справочная книга по математической логике. – M.:Наука. – 3.1.

1983.

(Барздинь Я.М.) 4.Барздинь [1981] Об индуктивных правилах вывода для синтеза программ // 4.1.

Синтез, тестирование, верификация и отладка программ.

Тезисы докл. всесоюзной научной конференции, Рига. – 1981. – С. 25-26.

[1983] Один подход к проблеме индуктивного вывода // Применение 4.2.

методов математической логики. Тезисы докл. всесоюзной научной конференции, Таллин. – 1983. – С.16-28.

и Горлин (Бухштаб Ю.А., Горлин А.И.) 5.Бухштаб [1982] Об одном методе планирования расчетных цепочек.

5.1.

// Программированиею – № 3. – 1982. – С.49-55.

(Вирт Н.) 6.Вирт [1977] Систематическое программирование. – М.:Мир. – 1977.

6.1.

(Воронков А.А.) 7.Воронков [1985] Метод поиска доказательства // Вычислительные системы.

7.1.

Новосибирск. – 1985. – т. Маслов (Давыдов Г.В., Маслов С.Ю.) 8.Давыдов, [1969] Машинный алгоритм установления выводимости на основе 8.1.

обратного метода // Записки ЛОМИ АН СССР. – 1969. – т.16. – с.8- Дейкстра (Дейкстра Э.) 9.

[1975] О структурной организации данных. – В кн.: Структурное 9.1.

программирование. – М.:Мир. – 1975.

(Диковский А.Я.) 10.Диковский [1983а] Оценки алгоритмов, связанных с вычислительными моделями 10.1.

// Применение методов математической логики. – Тезисы докладов Всесоюзной конференции. Таллин. – 1983. – C.42-51.

[1983б] Анализ и синтез алгоритмов над базисом функциональных 10.2.

зависимостей. // Оптимизация и преобразование программ, ч.1.

ВЦ СОАН СССР. – Новосибирск. – 1983. – C.140-152.

[1984] Детерминированные вычислительные модели // Техническая 10.3.

кибернетика. – 1984, № 5. – C.84-105.

(Драгалин А.Г.) 11.Драгалин [1979] Математический интуиционизм. Введение в теорию 11.1.

доказательств. – М.:Наука. – 1979.

и Прад (Дюбуа Д., Прад А.) 12.Дюбуа [1990] Теория возможностей. Приложения к представлению знаний в 12.1.

информатике. – М.:Радио и связь. – 1990. – 288 c.

(Заде Л.) 13.Заде [1976] Понятие лингвистической переменной и его применение к 13.1.

принятию приближенных решений. – М.:Мир. – 1976. – 162 c.

и Фараджев (Карзанов А.В., Фараджев И.А.) 14.Карзанов [1975] Планирование вычислений при решении задач на 14.1.

вычислительных моделях // Программирование, 1975. – № 4. – C. 19- и Поттосин (Касьянов В.Н., Поттосин И.В.) 15.Касьянов [1982] Системы конкретизации: подход и основные понятия. – 15.1.

Препринт ВЦ СО АН СССР, № 349. – Новосибирск. – 1982. – 22 C.

Каля и Тыугу (Кахро М. И., Каля А. П., Тыугу Э. Х.) 16.Кахро, [1981] Инструментальная система программирования ЕС ЭВМ 16.1.

(ПРИЗ). – М.:Финансы и статистика. – 1981. – 157 c.

(Кашуба Л.А.) 17.Кашуба [1998] Параллельное проектирование средствами CAD/CAM/CAE в 17.1.

жизненном цикле изделий машиностроения // Программные продукты и системы. – 1998. – №3. – C.24-31.

(Кофман А.) 18.Кофман [1977] Введение в теорию нечетких множеств. – М.:Радио и связь. – 18.1.

1977. – 432 C.

(Лавров С.С.) 19.Лавров [1982] Синтез программ // Кибернетика. – 1982, № 6. – C. 11-16.

19.1.

(Мартин Дж.) 20.Мартин [1980] Организация баз данных в вычислительных системах. – 20.1.

М.:Мир. – 1980. – 662 c.

(Маслов С.Ю.) 21.Маслов [1964] Обратный метод установления выводимости в классическом 21.1.

иcчислении предикатов. // ДАН СССР. – 1964. – вып.159, №1. – с. 17- [1966] Применение обратного метода к теории разрешимых 21.2.

фрагментов классических исчислений // ДАН СССР. – 1966. – №1. – С. 17-20.

[1967] Обратный метод установления выводимости для 21.3.

непредваренных формул исчисления предикатов // ДАН СССР.

– 1967. – №1. – С. 22-25.

[1968] Обратный метод установления выводимости для логических 21.4.

исчислений // Труды Математического института АН СССР. – 1968. – T.XCVIII. – C.26- [1969] Связь между тактиками обратного метода и метода резолюций.

21.5.

// Записки ЛОМИ АН СССР. – 1969. – T.16. – C.21- [1971] Обобщение обратного метода на исчисление предикатов с 21.6.

равенством // Записки ЛОМИ АН СССР. – 1971. – T.20. – C.80 [1972] О поиске вывода в исчисленьях общего типа. // Записки ЛОМИ 21.7.

АН СССР. – 1972. – T.32. – C.59– [1983а] Стратегии в резолютивном и обратном методе. // 21.8.

Математическая логика и автоматическое доказательство теорем. – М.: Наука. – 1983. – С. 327- и Минц (Маслов С.Ю., Минц Г.Е.) 22.Маслов [1983] Теория поиска доказательств и обратный метод. // 22.1.

Математическая логика и автоматическое доказательство теорем. – М.: Наука. – 1983. – С. 291- Бернштейн и Коровин (Мелихов А.С., Бернштейн Л.С., Коровин 23.Мелихов, С.Я.) [1990] Ситуационные советующие системы с нечеткой логикой. – М.:

23.1.

Наука. – 1990. – 271 с.

(Мендельсон Э.) 24.Мендельсон [1976] Введение в математическую логику. – М.: Наука. – 1976.

24.1.

(Минц Г.Е.) 25.Минц [1981] Резолютивные исчисления для неклассических логик // 9-ый 25.1.

Советский Кибернетический симпозиум, М.:ВИНИТИ. – 1981.

– T.2. – C.34- [1983] Структурный синтез рекурсивных программ // Автоматический 25.2.

синтез программ. – Таллин, 1983. – C. 58- и Тыугу (Минц Г. Е., Тыугу Э. Х.) 26.Минц [1982] Полнота правил структурного синтеза // Докл. АН СССР. – №4.

26.1.

– 1982.

[1983] Структурный синтез и неклассические логики. Применение 26.2.

методов математической логики. Таллин: 1983, с. 52-60.

(Нейман В. С.) 27.Нейман [1985] Синтез программ по описаниям рекурсивных отношений.

27.1.

Синтез программ // Тезисы докладов Всесоюзной школы семинара. – Устинов. – 1985. – C. 25-27.

(Непейвода Н.Н.) 28.Непейвода [1978] Соотношение между правилами естественного вывода и 28.1.

операторами алгоритмических языков высокого уровня // Докл.

АН СССР. – 1978, № 3 – C. 526-529.

[1979] Об одном методе построения правильной программы из 28.2.

правильных подпрограмм // Программирование, 1979, № 1, C. 15-25.

(Новосельцев В.Б.) 29.Новосельцев [1981] Алгоритм синтеза ветвящихся программ с квадратичной 29.1.

временной оценкой // Синтез, тестирование, верификация и отладка программ. Рига. – 1981. – C.168-171.

[1985a] Структурные вычислительные модели – формальный базис // 29.2.

Синтез программ. – ЦНТИ. – 1985. – С.74-76.

[1985б] Системы программирования с интеллектуальными 29.3.

возможностями. Методология системных исследований // Докл. Всес. симпозиума. – 1985. – С. 161-166.

[1985в] Синтез рекурсивных программ в системе СПОРА. Препринт 29.4.

ИТА АН СССР «Алгоритмы небесной механики», №43, Ленинград. – 1985. – 45 С.

и Аксенов (Новосельцев В.Б., Аксенов С.В.) 30.Новосельцев [2006] Организация и использования нейронных сетей. – Томск: НТЛ.

30.1.

– 2006. – 160 С.

и Бурлуцкий (Новосельцев В.Б., Бурлуцкий В.В.) 31.Новосельцев [2001] Реализация обратного метода для модальной логики KT // 31.1.

Исследования по анализу и алгебре. – Томск. – 2001. – С.57-66.

и Калайда (Новосельцев В.Б., Калайда В.Т.) 32.Новосельцев [1986] Концепции построения программного окружения для решения 32.1.

задач оптики атмосферы. // Ж. Оптики атмосферы. – М.:Радио и связь. – №6. – 1986. – С.43-51.

33.

Калайда и Шагисултанов (Новосельцев В.Б., Калайда В.Т., 34.Новосельцев, Шагисултанов В.Г.) [1991] Разработка программного обеспечения для представления 34.1.

управляемых объектов в системах связи. // Н/т. отчет № K5 14/91-г/б. – Томск: ИОА СО РАН. – 1991. – 76 С.

Колтун и Романчук (Новосельцев В.Б., Колтун П.Н., Романчук 35.Новосельцев, Е.А.) [2004] Возможность использования дескрипторных логик в системе 35.1.

управления знаниями // Вестник ТГУ (Математика.

Кибернетика. Информатика). – №284. – 2004. – с.17- и Ларионов (Новосельцев В.Б., Ларионов Д.С.) 36.Новосельцев [2002] Оболочка экспертной системы на основе нечетких рассуждений 36.1.

с прямым и обратным выводом // Математическое моделирование. – T.14, №9. – 2002. – С.48-52.

и Малахов (Новосельцев В.Б., Малахов А.В.) 37.Новосельцев [2004] К вопросу о синтезе параллельных алгоритмов // Вестник ТГУ 37.1.

(Математика, Кибернетика, Информатика), №284. – 2004. – с.35- и Романчук (Новосельцев В.Б., Романчук Е.А.) 38.Новосельцев [2005] О манипулировании знаниями с использованием нечетких 38.1.

множеств (личный вклад С.44-47) // Ж.Оптика атмосферы и океана (Юбилейный выпуск). – №4. – 2005. – с.44- и Тютерев (Новосельцев В.Б., Тютерев В.В.) 39.Новосельцев [2001] Метод динамического наращивания узлов как способ 39.1.

построения нейронных сетей эффективного размера. // Ж.

Нейрокомпьютеры: разработка и применение. – Радиотехника, №2, 2001. – с.82- (Опарин Г.А.) 40.Опарин [1981] К теории планирования вычислительного процесса в пакетах 40.1.


прикладных программ // Пакеты прикладных программ.

Новосибирск: Наука. – 1981. – с. 5- (Оре О.) 41.Оре [1980] Теория графов. – М.: Наука. – 1980. – 336 C.

41.1.

(Поспелов Д.А) 42.Поспелов [1981] Логико-лингвистические модели в системах управления. – М.:

42.1.

Энергоиздат. – 1981. – 231 C.

(Робинсон Дж.) 43.Робинсон [1970] Машинно-ориентированная логика, основанная на принципе 43.1.

резолюции // Кибернетический сборник, Новая серия. – М.:

Мир. – 1970, вып. 7. – с. 194- и Юсупов (Смирнов А.В., Юсупов Р.М.) 44.Смирнов [1992] Совмещенное проектирование: необходимость, проблемы 44.1.

внедрения, перспективы. – СПб: СПИИРАН. – и др. (Тейз А., Грибомон П., Ж. Луи и др.) 45.Тейз [1990] Логический подход к искусственному интеллекту. т.1. От 45.1.

классической логики к логическому программированию. – М.:Мир. – [1998] Логический подход к искусственному интеллекту. т.2. От 45.2.

модальной логики к логике баз данных. – М.: Мир. – (Тарасов В.Б.) 46.Тарасов [1993] Интеллектуальные системы в проектировании // Новости 46.1.

искусственного интеллекта. – 1993. – №4. – с.24- (Тыугу Э. Х.) 47.Тыугу [1970] Решение задач на вычислительных моделях // ЖВМ и МФ, 47.1.

1970, 10, № 3, с. 716- (Ульман Дж.) 48.Ульман [1983] Основы систем баз данных. – М.: Финансы и статистикА. – 48.1.

1983. – 334 C.

(Фейс Р.) 49.Фейс [1974] Модальная логика. – М.: Наука. – 49.1.

(Харф М. Я.) 50.Харф [1983] Реализация синтезатора программ в системе 50.1.

программирования ПРИЗ // Автоматический синтез программ.

Таллин, 1983, с. 110- [1984] Исследование и реализация методов структурного синтеза 50.2.

программ. – Дисс. канд. техн. Наук. ИК АН ЭССР, Таллин, (Хоор К.) 51.Хоор [1975] О структурной организации данных. Структурное 51.1.

программирование. – М.: Мир. – 1975. – с.98- и Ли (Чень Ч., Ли Р.) 52.Чень [1983] Математическая логика и автоматическое доказательство 52.1.

теорем. – М.: Наука. – 1983. – 360 C.

(Ягер Р.) 53.Ягер [1986] Нечеткие множества и теория возможностей, последние 53.1.

достижения M.: Радио и связь. – 1986. – 406 C.

Enjalbert and Hebrard (Auffray I., Enjalbert P., Hebrard J.-J.) 54.Auffray, [1990] Strategies of modal resolution: Results and problems // Journal of 54.1.

Automated Reasoning – 1990 – vol.9 – pp. 1- and Hollunder (Baader F., Hollunder B.) 55.Baader [1991] A terminological knowledge representation system with complete 55.1.

inference algorithm’s // PDK’91, Boley H. And Richter M. Eds., Lecture Notes in Artificial Intelligence. vol.567, Springer Verlag. – 1991. – pp.67- and Gansinger (Bachmair L. Gansinger H.) 56.Bachmair [2000] Resolution theorem proving. – Handbook of Automated reasoning, 56.1.

(Robinson A. And Voronkov A. – Eds). – Elsevier science and MIT Press. – Heuerding and Schwendimann (Balsiger P., Heuerding A., 57.Balsiger, Schwendimann S.) [1998] Logics Workbench 1.0 // Automated Reasoning with Analytic 57.1.

Tableaux and Related Methods, International Conference, TABLEAUX’98 H. De Swart Ed. Lecture Notes in Artificial Intelligence. vol.1397, Springer Verlag. – 1998. – pp.35- and Krishnaswamy (Bierman A. W., Krishnaswamy R.) 58.Bierman [1976] Constructing programs from example computations // IEEE Trans.

58.1.

On Software Engineering, 1976, vol. SE-2, № 2, pp. 141- Grader and Gurevich (Borger E., Grader E., Gurevich Y.) 59.Borger, [1997] The Classical Decision Problem. – Springer Verlag – 59.1.

(Borgida A.) 60.Borgida [1995] Description logics in data management // IEEE Transactions on 60.1.

Knowlede and Data Engineering, 7(5), October [1996] On the relative expressiveness of description logics and predicate 60.2.

logics // JAIR, 82(1996), pp. 353- wen (Bowen K.) 61.Bo [1979] Model Theory for Modal Logics // Syntheses Library. vol.128 – 61.1.

achman and others (R.Brachman, P.Sefridge, L.Terveen and others) 62.Br [1993] Knowledge representation support for data archeology // Int. J. of 62.1.

Intelligent and Cooperative Information Systems 2(2), June 1993. – pp.159- and Darlington (Burstall R. M., Darlington J.) 63.Burstall [1976] A system which automatically improves programs // Acta 63.1.

Informatica, vol. 6. – 1976. – pp. 41 - 60.

[1977] A Transformation system for developing Recursive Programs // 63.2.

Journal of the ACM, vol. 24. – 1977. – pp. 44- chheit and others (Buchheit M., Manfred A. and others) 64.Bu Subsumption between Queries to Object-Oriented Databases // 64.1. [1997] JAIR, 86(1997) – lvanese and other (Calvanese D., De Giacomo G., Lenzerini M., Nardi D.) 65.Ca [2000] Reasoning in expressive description logics // Handbook of 65.1.

Automated reasoning, Robinson A. And Voronkov A. Eds. Elsevier science and MIT Press. – (Catach L.) 66.Catach [1991] Tableaux: a general theorem prover for modal logics // Journal of 66.1.

automated reasoning. – 1991. – vol.7, №4. – pp.489- and Zakharyaschev (Chagrov A., Zakharyaschev M.) 67.Chagrov [1996] Modal Logic- 1996 – Oxford University Press 67.1.

(Constable R. L.) 68.Constable [1972] Constructive mathematics and automatic program writers // Proc.

68.1.

IFIP 1971, North-Holland, 1972, pp. 733- (Curry H.) 69.Curry [1963] Foundations of Mathematical Logic – 1963. – McGraw-Hill, New 69.1.

York (Davis M.) 70.Davis [1962] Eliminating the Irrelevant from Mechanical Proofs // Proc. Symp.

70.1.

On Experimental Arithmetic, Chicago, - 1962.

and Voronkov (Degtyarev A., Voronkov A.) 71.Degtyarev [1994а] Equality elimination for the semathic tableax// UPMAIL Technical 71.1.

Report 90, Uppsala University, Computing Science Department – [1994б] Equality elimination for the inverse method and extension 71.2.

procedures // UPMAIL Technical Report 92, Uppsala University, Computing Science Department – [1995] Equality elimination for the inverse method and extension 71.3.

procedures // Proc. International Joint Conference on Artificial Intelligence (IJCAI), C. Mellish ed., Montreal. – 1995. – vol.1. – pp.342- [1996а] Equality elimination for the tableau method // Design and 71.4.

Implementation of Symbolic Computation Systems. International Symposium, DISCO’96 J.Calmet, C.Limongelli Eds., Lecture Notes in Computer Science. – 1996. – vol.1128, Springer Verlag. – pp.46- [1996б] The undecidability of simultaneous rigid E-unification// 71.5.

Theoretical Computer Science – 1996. – vol.166, №1-2. – pp.291 (Fitting M.) 72.Fitting [1983] Proof methods for modal and intuicionistic logics. Synthesis 72.1.

Library, 1983, vol. 169. Reidel Pub. Comp.

[1996] First Order Logical Automated Theorem Proving. – 1996 – Springer 72.2.

Verlag, New-York, Second Edition and Mendelsohn (Fitting, M., Mendelsohn R.) 73.Fitting [1998] First-Order Modal Logic 1998 – Kluwer Academic Publishers 73.1.

Thalmann and Voronkov (Fitting, M., Thalmann L., Voronkov A.) 74.Fitting, [2000] Term-modal logics // Automated Reasoning with Analytic Tableaux 74.1.

and Related Methods (TABLEAUX – 2000), Dyckhoff R. Ed.

Lecture Notes of Artificial Intelligence, Springer Verlag – 2000 – vol. 1847 – pp.220- (Friedman J.A.) 75.Friedman [1963] Semi-decision procedure for the functional calculus // Journal of 75.1.

ACM. – 1963. – vol. 10, №1. – pp.1- and Guenther (Gabbay D., Guenther F.) 76.Gabbay [1984] Handbook on Philosophical Logic. – Reidel, Dordrecht. – 76.1.

(Gentzen. G.) 77.Gentzen [1934] Untersuchungen uber das logische Schliessen. Mathematishe 77.1.

Zeitschrift, vol.39. – 1934. – pp.176- Lafont and Taylor (Girard J.-Y., Lafont Y., Taylor P.) 78.Girard, [1989] Proofs and types – 1989. – Cambridge University Press 78.1.

and Sebastiani (Giuchinglia F., Sebastiani R.) 79.Giuchinglia [1996а] Building decision procedures for modal logics from propositional 79.1.

decision procedure: Case study of modal K // CADE-13, M.McRobbie and J.Slaney, Eds. Lecture Notes in Computer Science – 1996. – vol.1104. – pp.583- [1996б] SAT-based decision procedure for ALS // KR’96 – 1996. – pp.304 79.2.

(Giuchinglia F.) 80.Giuchinglia [1998] More evaluation of decision procedures for modal logics // 80.1.

Principles of Knowledge Representation and Reasoning:

Proceedings of the Sixth International Conference (KR’98), A.

Cohn, L. Schubert and S. Shapiro Eds. Morgan Kaufmann San Francisco, CA. – 1998. – pp.616- [1999] SAT-based decision procedures for classical modal logics // Journal 80.2.

of automated reasoning. – 1999. – To appear in the Special Issues:

Satisfy-ability at the start of the year 2000.

(Goble L.) 81.Goble [1974] Gentzen system for modal logic // Notre Dame Journal of Formal 81.1.

Logic – 1974 – vol.15 – pp.455- (Goldblatt. R.) 82.Goldblatt [1987] Logics of time and Computation // Lecture Notes, Center for the 82.1.

Study of Language and Information. – 1987. – № P.J.Veerkamp. – Berlin: Springer Verlag, 1991. – pp.3-19.

82.2.

and Harf (Grossschmidt G., Harf M.) 83.Grossschmidt [2001] Simulation of an electro-hydraulic servo-valve in NUT 83.1.

Programming Environment //Proc. of the 13th European Simulation Symposium "Simulation in Industry" ESS'2001, October 18–20, 2001, Marseille, France, pp. 229-233.

Moller and Turhan (Haarslev V., Moller R., Turhan A.-Y.) 84.Haarslev, [1998] Implementing in ALSRP(D) A Box Reasoner-progress report// Proc.

84.1.

DL’98 International Description Logic Workshop – (Hardy S.) 85.Hardy [1975] Synthesis of LISP functions from examples //4th IJCAI, Tbilisi, 85.1.

1975, pp. 240- (Harf M.) 86.Harf [1994] Structural Synthesis of Programs Using Regular Data Structures.

86.1.

//Proc. of the 6-th Nordic Workshop on Programming Theory, October 17-19, 1994, Aarhus, Denmark, 1994, pp. 194- (Heeffer A., – editor) 87.Heeffer [1986] Non-classical logics for expert systems. CC-AI, vol. 3, № 1-2, 1986.

87.1.

(Herbrand J.) 88.Herbrand [1930] Recherches sur la theorie de la demonstration. – Warsaw, 1930.

88.1.

(Horrocks I.) 89.Horrocks [1997] Optimizing tableaux decision procedure for modal logic// Ph.D.

89.1.

thesis University of Manchester. – [1998] Using expressive description logic: FACT or fiction? // Principles of 89.2.

Knowledge Representation and Reasoning: Proceedings of the Sixth International Conference (KR’98), A. Cohn, L. Schubert and S. Shapiro Eds. Morgan Kaufmann San Francisco, CA. – 1998. – pp.636- and Patel-Schneider (Horrocks I., Patel-Schneider P.) 90.Horrocks [1998] FACT and DLP//Automated Reasoning with Analytic Tableaux and 90.1.

Related methods. International conference TABLEAUX’98, H. de Swart Eds. Lecture Notes in Artificial Intelligence. – 1998. – vol.1397, Springer Verlag. – pp.27- [1999] Optimizing description logic subsumption/ Journal of Logic and 90.2.

Computation – 1999 – vol.9(3) – pp. 267- Patel-Schneider and Sebastiani (Horrocks I., Patel-Schneider P., 91.Horrocks, Sebastiani R.) [2000] An analysis on empirical testing for modal decision procedures.// 91.1.

Logic Journal of the IGPL – 2000 - vol. 8, №3 – pp. 293-323.

and Shmidt (Hustadt U., Shmidt R.) 92.Hustadt [1997] On evaluating decision procedures for modal logic.// IJCAI-97. – 92.1.

1997. – vol.1. – pp.202- and Bennet (John and Bennet) 93.John Language as a self organized system // Cybernetic and ssssssystems, v.2. – 93.1.

1982. – pp. 201- (Kanger S.) 94.Kanger [1983] A simplified proof method for elementary logic. // Automated of 94.1.

Reasoning. Classical Papers of Computational Logic, Siekmann J., Wrightson G. Eds., Springer Verlag – 1983 – vol.1 – pp. 364- Levy and Pfeffer (Koller D., Levy A., Pfeffer A.) 95.Koller, [1997] P-CLASSIC: A tractable probabilistic description logic // 95.1.

Proceedings of the Fourteenth National Conference on Artificial Intelligence (AAAI-97), – 1997. – pp. 390- (Kripke S.A.) 96.Kripke [1971] Semantical considerations on modal logic. // Reference and 96.1.

Modality, Oxford University Press, London. – 1971. – pp. 63- (Kuechner D.) 97.Kuechner [1971] A note on the relation between resolution and Maslov’s inverse 97.1.

method. // Machine Intelligence, Melzer B., Michie D. Eds., American Elsiver – 1971 – vol.6 – pp.73- (Lakoff G.) 98.Lakoff [1972] Linguistics and natural logic // Semantics for Natural Language. – 98.1.

Reidel, Dordrecht. – 1972.

and Chase (D. B. Leblang and J. R. P. Chase) 99.Leblang [1984] Computer-Aided Software Engineering in a Distributed Workstation 99.1.

Environment // Proc. ACM SIGSOFT/SIGPLAN Software Engineering Symposium on Practical Software Development Environments, Pittsburgh, PA, April, 1984, pp. 104- (Lifschitz V.) 100.Lifschitz [1989] What is the inverse method? // Journal of Automated reasoning, 100.1.

vol.5(1), 1989. – pp.1- Sattler and Tobies (Luntz C., Sattler U., Tobies S.) 101.Luntz, [1995] A Suggestion for n-ary Description Logic. // www.air.dom.edu. – 101.1.

and Waldinger (Manna Z., Waldinger R.) 102.Manna [1977] The automatic synthesis of recursive programs. SIGPLAN Notice, 102.1.

1977, 12, № 8, pp. 29- (Mints G.) 103.Mints [1993] Resolution calculus for the first order linear logic// Journal of 103.1.

Logic, Language and Information. – 1993. - №2. – pp.58- [1994] Resolution strategies for intuitionistic logic// Constraint 103.2.

Programming. NATO ASI Series F. Springer Verlag – 1994 – pp.

289- Voronkov and Degtyarev (Mints G., Voronkov A., Degtyarev A.) 104.Mints, [2000] Inverse method. // Handbook of Automated reasoning, Robinson A.

104.1.

And Voronkov A. Eds. Elsevier science and MIT Press. – Orevkov and Tammet (Mints G., Orevkov V., Tammet T.) 105.Mints, [1996] Transfer of sequent calculus strategies to resolution for S4// Proof 105.1.

Theory of Modal logic. Studies in Pure and Applied logic, Kluwer Academic Publishers. – and Rubio (Niewenhuis R., Rubio A.) 106.Niewenhuis [2000] Paramodulation-based theorem proving. // Handbook of Automated 106.1.

reasoning, Robinson A. And Voronkov A. Eds. Elsevier science and MIT Press. – (Patel-Schneider P.) 107.Patel-Schneider [1998] DLP-system description. // Proc. DL’98 International Description 107.1.

Logic Workshop –1998 – pp. 87- and others (Rector A.L., Bechhofer S.K. and others) 108.Rector [1997] The GRAIL Concept Modeling Language for Medical 108.1.

Terminology. // Artificial Intelligence in Medicine. V. 9, 1997. – pp. 139- (Robinson J.) 109.Robinson [1964] On automatic deduction. // Rice Univ. Studies. – 1964. – vol.50, 109.1.

№1. – pp. 69- (Schmidt R.) 110.Schmidt [1998] Resolution in a decision procedure for many propositional modal 110.1.

logics. // Advances in Modal Logics, Kracht M., de Rijhte M., Zakharyaschev M. Eds., Lecture Notes, CSLI Publications – 1998 – vol. 87 – pp. 189- (Tachella A.) 111.Tachella [1999] *SAT system description. // Proceedings of the 1999 International 111.1.

Description Logic Workshop (DL’99), P.Lambrix, A.Borgida, M.Lenzerini, R.Moller and P.Pattel-Schneider, Eds. CEUR-WS. – 1999. – vol.22. – pp.142- (Tammet T.) 112.Tammet [1994] Proof strategies in linear logic. // Journal of automated reasoning. – 112.1.

1994. – vol.12, №3. – pp.273- [1996] A resolution theorem prover for intuitionistic logic. //CADE-13, 112.2.

M.McRobbie and J.Slaney, Eds. Lecture Notes in Artificial Intelligence. – 1996. – vol.1104, Springer Verlag. – pp.2- (Tougu H.) 113.Tougu [1980] Towards practical synthesis of programs. Information Processing 113.1.

80, Amsterdam: North- Holland Publ. Co., 1980, pp. 207- (Treur J.A.) 114.Treur [1991] A Logical Framework for Design Processes// Intelligent CAD 114.1.

Systems III: Practical Experience and Evaluation/ Ed. by P.J.W.

(Voronkov A.) 115.Voronkov [1992] Theorem proving in non-standard logics based on the inverse 115.1.

method. 11h international Conference on Automated Deduction, D.Kapur, Ed. Lecture Notes in Artificial Intelligence, 1992, vol.

607. Springer Verlag, pp.648– [1999] K-inverse-K: a theorem prover for K // Automated Deduction.

115.2.

CADE-16, International Conference on Automated Deduction, H.Ganzinger Eds. Lecture Notes in Artificial Intelligence. vol.1632, Springer Verlag. – 1999. – pp.383- [2000] How to optimize proof-search in modal logics: new methods of 115.3.

proving redundancy criteria for sequent calculi // LICS’ [2001] How to optimize proof-search in modal logics // ACM Transactions 115.4.

and Computational logic, vol.1 – 2001. – pp.1- and Lee (Waldinger R. J., Lee R. C. T.) 116.Waldinger // Proc. of the 1st [1969] A step toward automatic program writing.

116.1.

International Joint Conference on Artificial Intelligence, Bedford. – 1969. – pp. 241- (Wallen. L.) 117.Wallen [1990] Automated deduction in nonclassical logics. – The MIT Press. – 117.1.

and other (Weidenbach et al.) 118.Weidenbach [1996] SPASS & FLOTTER version 0.42 // CADE-13, M.McRobbie and 118.1.

J.Slaney, Eds. Lecture Notes in Artificial Intelligence, vol.1104, Springer Verlag. – 1996. – pp.141- Wirth (Wirth N.) 119.

[1971] The programming language Pascal. // Acta Informatica, vol.1 – 119.1.

1971, – pp.35-63.

(Yoshikawa H.) 120.Yoshikawa [1989] General Design Theory as a Formal Theory of Design // In:

120.1.

Intelligent CAD. – Amsterdam: Elsevier Sci. Publishers, 1989. – pp.51-61.



Pages:     | 1 | 2 ||
 





 
© 2013 www.libed.ru - «Бесплатная библиотека научно-практических конференций»

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