Теория вывода в многозначных логиках

Комендантский, Владимир Евгеньевич

автореферат диссертации по философии, специальность ВАК РФ 09.00.07
диссертация на тему: Теория вывода в многозначных логиках

Год: 2003
Автор научной работы: Комендантский, Владимир Евгеньевич
Ученая cтепень: кандидата философских наук
Место защиты диссертации: Москва
Код cпециальности ВАК: 09.00.07

Диссертация по философии на тему 'Теория вывода в многозначных логиках'

Полный текст автореферата диссертации по теме "Теория вывода в многозначных логиках"

Российская Академия Наук Институт философии

На правах рукописи

КОМЕНДАНТСКИЙ Владимир Евгеньевич

ТЕОРИЯ ВЫВОДА В МНОГОЗНАЧНЫХ ЛОГИКАХ

Специальность 09.00.07 Логика

АВТОРЕФЕРАТ диссертации на соискание учёной степени кандидата философских наук

Москва 2003

Работа выполнена в секторе логики Института философии Российской Академии Наук (ИФ РАН).

Научный руководитель:

доктор философских наук КАРПЕНКО Александр Степанович

Официальные оппоненты:

доктор физико-математических наук АНШАКОВ Олег Михайлович,

кандидат философских наук КАТРЕЧКО Сергей Леонидович

Ведущая Кафедра логики философского

организация: факультета Московского

Государственного Университета.

Защита состоится 23 октября 2003 г. в 16:00 на заседании диссертационного совета Д 002.015.03 ИФ РАН по адресу: 119992 Москва, ул. Волхонка, д. 14, Институт философии, зал заседаний.

С текстом диссертации можно ознакомиться в библиотеке Института философии.

Автореферат разослан «23 » сентября 2003 г.

Учёный секретарь КИЯЩЕНКО

диссертационного совета Лариса Павловна

доктор философских наук

Общая характеристика диссертации

Многозначные логики появились в 20-х годах XX века в работах Поста и Лукасевича. Несколько позднее было предложено ещё несколько многозначных логик, таких как логика Бочвара, логики Гёделя, логика Клини. Интересный библиографический экскурс в многозначные логики можно найти в [3]. Изобретение этих логик было мотивировано разными задачами. Так, Лукасевич и Бочвар исходили из философских предпосылок, вводя третье значение в свои логики для формализации неполного или противоречивого знания; Пост и Гёдель руководствовались более техническими соображениями, когда обобщали классическую логику в п-значных системах; Клини же просто искал удобный формализм для анализа понятия частично определённой рекурсивной функции. Однако все эти логики объединяет важная отличительная особенность: в них метатеоретически заложена концепция, которую называют истинностной функциональностью. Согласно ей, всякое высказывание имеет некоторое значение истинности, и это значение может быть однозначно вычислено некоторой заранее определённой функцией по значениям входящих в это высказывание подвысказыва-ний. Так, в случае конъюнкции А А В высказываний А и В искомой функцией будет некоторая функция /л от значения А и значения В.

РоС ' г (ДЛЬМАЯ

: •> > ^

по любой формуле можно легко сказать, что она «значит». Сохраняется ли эта привлекательность многозначных логик в теории вывода? К сожалению, нет, поскольку с ростом числа истинностных значений растёт и то внимание, которое им приходится уделять, а в это время падает эффективность рассуждений.

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

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

Актуальность темы диссертации. Сегодня для бес-конечнозначных логик не существует хорошо обоснованной теории доказательств, хотя для конечнозначных логик табличные исчисления без сечений были построены ещё Руссо [15] в 1967 году. Некоторые исчисления для бес-конечнозначных логик Лукасевича всё же определяются в литературе, например, Агуццоли и Чиабаттони [9] в 2000 году строят секвенциальное исчисление для беско-нечнозначной логики, опирающееся на идею Мундичи о сводимости проблемы разрешимости с бесконечнозначной логики на подходящий класс конечнозначных логик, и, следовательно, основанное на исчислениях для конечнозначных логик. В 2001 году Софрони-Стоккерманс [17] предложила метод доказательства теорем, основанный на теореме представления алгебр истинностных значений для большого класса многозначных логик. Кроме своей эффективности, этот метод интересен ещё и тем, что в нём посредством структур Крипке устанавливается соответствие между многозначными и модальными логиками. К сожалению, метод [17] неприменим к ряду широко распространённых бесконечнозначных логик. Данный метод исследован в диссертации, и на основе этого исследования сделан вывод о возможности его обобщения на класс бесконечнозначных логик на основе подходящей теоремы представления алгебр истинностных значений.

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

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

Методы исследования. В работе использовалась логическая техника, как традиционная, например, секвенциальные логические исчисления, так и нетрадиционная: исчисления с «отмеченными формулами», 5-классификация замкнутых классов функций многозначных логик, дуальные многозначным семантикам топологические модели. Автором работы вводится оригинальный метод на основе исчисления резолюций для доказательства теорем в многозначных логиках с линейно упорядоченными множествами истинностных значений.

Основные результаты работы и положения, выносимые не защиту:

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

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

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

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

Научная новизна работы состоит в том, что в ней

• предпринята попытка целостного философского анализа феномена символических систем многозначных логик — от их возникновения в первой четверти XX века до наших дней;

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

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

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

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

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

разнообразных задачах управления, например, в задачах управления сложными процессами, не имеющими простых математических моделей, таких как нелинейные процессы, а также в задачах обработки баз знаний, сформированных языковыми данными, полученными от экспертов. Приведём для наглядности некоторые промышленные реализации систем управления на основе нечётких логик: производство полупроводников (Canon), оптимизирование автобусных расписаний (Toshiba), система архивации документов (Mitsubishi Electric), система раннего предсказания землетрясений (Ин-т сейсмологии, Япония), диагностика раковых заболеваний (Kawasaki), распознавание написанных от руки текстов карманными компьютерами (Sony), однокнопочная система управления для стиральных машин (Matsushita, Hitachi), ядерные реакторы повышенной безопасности (Hitachi, Bernard), симуляция судебных разбирательств (ун-т г. Нагоя, Япония).

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

• Смирновские чтения 3, сектор логики ИФ РАН, 2001 г.;

• Современная логика: проблемы теории, истории и применения в науке, СПбГУ, 2002 г.;

• 14th European Summer School for Logic, Language and Information, Тренто, Италия, 2002 г.;

• Смирновские чтоиия 4, сектор логики ИФ РАН, 2003 г.;

• Summer School and Workshop on Proof Theory, Computation and Complexity, Дрезден, Германия, 2003 г.

Структура и объём работы. Диссертация состоит из введения, семи глав, заключения, приложения и списка литературы.

Основное содержание диссертации

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

В первой главе — «Истинностно-функциональные семантики» — осуществляется содержательное философское истолкование концепции истинностной функциональности, лежащей в основе явления многозначности. Раскрывается понятие истинностно-функциональной семантики, приводятся наиболее распространённые варианты таких семантик, и среди них: семантика голосования, семантика сходства, семантика рисков, семантика допустимости, семантика приближений.

Во второй главе — «Формализация многозначных логик» — даются строгие определения понятий многозначной теории вывода, таких как: логика высказываний, логика первого порядка, абстрактная алгебра, логический

вывод, формула с метками, логическое исчисление (секвенциальное, табличное, гильбертовское, резолютивное).

Третья глава — «Функциональный анализ многозначных логик» — содержит изложение основных результатов анализа и классификации функций многозначных логик в классе функций п-значных логик Поста. Приводятся определения замкнутых и ¿'-замкнутых классов функций многозначных логик, а также критерии полноты и 5-полноты для этих классов. Даётся предикатная характеризация 5-замкнутых классов по Марченкову. Перечисляются функциональные свойства известных многозначных логик.

Четвёртая глава — «Метод резолюций для смешанной логики Поста» — посвящена исследованию так называемой смешанной логики Поста Ро&Ы/, предложенной Косовским и Тишковым [5], и обобщающей в своём исчислении свойства класса исчислений всех п-значных логик Поста. В главе строится исчисление резолюций в духе [10] для смешанной логики Поста.

У логики РовЬЬ есть два уровня. На первом, внутреннем, уровне рассматриваются формулы многозначной логики. Множество истинностных значений и интерпретация логических связок определяются во внутренней сигнатуре. Предметные переменные — многосортные. На втором, внешнем, уровне имеется единственный предикат сравнения значения внутренних формул с нулём. Внешний язык не содержит функциональных символов. Множество внешних предметных переменных совпадает с множеством внутренних предметных переменных. Формулы второго уровня — это формулы двузначной (классической) логики.

Благодаря тому, что для любой PosiL-формулы можно построить сколомизированную классическую КНФ (также мы будем называть её множеством дизъюнкций PostL), мы получаем схему правила резолюции. Пусть -< обозначает одно из отношений ^ или < на рациональных числах. Здесь мы предполагаем, что любой 2-значный литерал (0 -< А[+В]) (т.е. формула внешнего уровня с отрицаниями или без), входящий в дизъюнкцию литералов PostL, является сколемизированной формулой, получающейся с помощью конечного числа применений специальной функции перевода 5 (она определена в тексте) к некоторой PosiL-формуле, А и В — это атомы (элементарные формулы) внутреннего уровня, с отрицаниями или без. Выражения в квадратных скобках (с одинаковыми индексами, если они присутствуют), при чтении можно одновременно опустить.

Определение (Резолюция). Пусть Дх и Д2 — дизъюнкции со сколемизированными литералами вида (0 -< А[+В}), тогда бинарная резолюция — это правило

Аг U {(0 Л1[+Б]1)} Д2 U {(0 -< ->А2[+С\2)} (ДгиДги^О^ВН+СТО)*

где знак -< в заключении обозначает ^ тогда и только тогда, когда -< — это ^ в обеих посылках, в противном случае -< обозначает <; а — это наиболее общий унификатор формул А\ и А2. В и С — это атомы, возможно пустые; в частности, если оба эти атома пусты, мы получаем пустую дизъюнкцию литералов 0 -< 0.

Вместе с бинарной резолюцией мы допускаем использование правила (-< Split), что позволяет перегруппировы-

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

А У (0 < А + ->А) А и (0 < 0)

Лемма (Основные дизъюнкции литералов). Пусть Ф — произвольное множество основных дизъюнкций литералов РовЬЬ. Если Ф невыполнимо, то пустая дизъюнкция (О -< 0) выводима из Ф конечным числом применений правила бинарной резолюции.

Лемма (подъёма). Если Д^ и Ы2 — это подстановочные случаи дизъюнкций литералов А-\ и Д2 соответственно, и если Д' — это резольвента Д'х и А'2, тогда существует резольвента Д дизъюнкций Дх и Д2, такая что Д' есть подстановочный случай Д.

Теорема (Полнота и непротиворечивость). Множество Ф дизъюнкций литералов РовЬЬ невыполнимо, если и только если пустой дизъюнкт (0 -< 0) выводим из Ф конечным числом применений правила бинарной резолюции.

Как следствие теоремы о полноте мы получаем результат:

Следствие. Проблема выполнимости в РовЬЬ полна в классе проблем, разрешимых на недетерминированной машине Тьюринга полиномиальными по времени алгоритмами.

В пятой главе — «Теорема Чена» впервые на русском языке даётся полное оригина. Iьиое доказательство теоремы Чена о полноте бесконечнозначной чогики Лука-севича относительно многообразия М\'-алгебр.

Лемма (компактности). Тождество Е имеет силу в линейно упорядоченной МУ-алгебре ([0,1], ф, О, ->, 0,1) тогда и только тогда, когда оно имеет силу в каждой линейно упорядоченной МУ-алгебре.

Теорема (Чен). В бесконечнозначной логике Лукасевича всякая формула общезначима, если и только если она доказуема.

Даже в статье Чена [13], где он доказывал эту теорему алгебраическим способом, доказательство не было самодостаточным. Мы приводим полное самодостаточное доказательство теоремы с доказательствами необходимых лемм. Теорема Чена используется далее в главе 6 при получении результата об ограниченности класса многозначных логик, относительно которых корректен специфический метод резолюций, описываемый в той же главе.

Шестая глава — «Метод резолюций на основе теоремы представления дистрибутивных решёток с операторами» — освещает проблематику представления алгебр многозначных логик и знакомит с методом поиска доказательства теорем многозначных логик, основанном на результате [16]. В данной главе мы исследуем теорию вывода многозначных логик с алгебраической точки зрения. Целью исследования является формулировка критерия применимости к произвольной многозначной логике предложенного в [17] метода резолюций на основе теоремы

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

Так называемые естественные теоремы представления (см. [18]), к которым относится и теорема Пристли, мотивированы следующими соображениями. Пусть Ь — это некоторая логика. Если Ь полна и непротиворечива относительно класса М матриц, и этот класс матриц может быть представлен как множество подмножеств реляционных структур в классе И, тогда реляционные структуры в И являются возможными кандидатами для определения класса Км,я моделей Крипке для Ь. В частности, при определённых условиях полнота и непротиворечивость логики Ь относительно класса Кмд е<"ть прямое следствие полноты и непротиворечивости Ь относительно М.

Ниже мы приведём основные понятия, необходимые для формулировки базовой теоремы [18, 16].

Непустое множество Ь с определёнными на нём двухместными операциями А и V называется решёткой, если

Л и V ассоциативны, коммутативны, идемпотентны и удовлетворяют законам поглощения. Дистрибутивной решёткой называется решётка, удовлетворяющая законам дистрибутивности А относительно V, а также V относительно Л.

Непустое подмножество Р решётки А называется фильтром, если для любых х,у £ Р имеет место хЛу Е Р, и для любых х,у £ Л, если ж 6 .Р и х у, тогда у Е Р. Фильтр Р1, максимальный относительно свойства 0 ^ Р. называется ультрафильтром. Фильтр ^ называется главным, если F ф А и для всех х,у е А, если х V у € тогда х Е Р или у £ Р. Далее, назовём порядковым фильтром множество Рх = {у : у х}, где х,у £ Ь.

Множество Л называется замкнутым, если оно содержит все объединения любых своих подмножеств, и открытым — если его дополнение замкнуто. Обозначим операцию замыкания произвольного множества как С. Множество с определённой на нём операцией замыкания называется пространством.

Класс В открытых подмножеств пространства X называется базисом X, если каждое открытое подмножество X есть объединение некоторых множеств, принадлежащих В. Класс Во открытых подмножеств пространства X называется подбазисом X, если класс В, состоящий из пустого множества 0, самого пространства X и всех конечных пересечений вида Вх П • • • П В„, где Вь ..., Вп £ В0, есть базис пространства X.

Пусть X и У — пространства. Взаимно однозначное отображение / : X —> У, сохраняющее операцию замыкания, т.е. удовлетворяющее /(С(А)) = С(/(А)), для

каждого множества А £ X, и /~1(С(В)) = С(/~1(В)), для каждого В С У, называется гомеоморфизмом X на У.

Определим дуал Пристли для ограниченной дистрибутивной решётки А как частично упорядоченное топологическое пространство О(А) = (^Р(Л),С,г), где FP(Л) — это множество главных фильтров на Л, а г — это топология, т.е. система замкнутых подмножеств, порождённая подбазисом, состоящим из множеств вида Ха = {Р € FP(.4) : а Е Р}, для всех а £ А, а также из их дополнений.

Пусть А — это ограниченная дистрибутивная решётка. Гомоморфизмом (антиморфизмом) на А называется функция к : А —> А, сохраняющая (обращающая) порядок. Гемиморфизмом относительно дизъюнкции на А называется функция / : Ап —> А, принимающая значение О, если любой её аргумент принимает значение 0, и, если её г-тый аргумент равен V 02, равная дизъюнкции двух функций /, у которых на г-тых аргументных местах находятся О] и а2 соответственно. Гемиморфизм относительно конъюнкции определяется двойственным образом: в предыдущем определении 0 заменяется на 1, а дизъюнкция — на конъюнкцию. Гемиантиморфизмом относительно дизъюнкции на А называется функция д : Ап —^ А, принимающая значение 0, если любой её аргумент принимает значение 1, и, если её г-тый аргумент равен щ А 0,21 равная дизъюнкции двух функций д, у которых на г-тых аргументных местах находятся а\ и а2 соответственно. Гемиантиморфизм относительно конъюнкции также определяется двойственным образом.

Обозначим как Е класс всех гомоморфизмов, антимор-

физмов, геми(анти)морфизмов относительно дизъюнкции и геми(анти)морфизмов относительно конъюнкции на произвольной ограниченной дистрибутивной решётке А.

Теорема (Теорема представления Пристли, [16]).

Каждая ограниченная дистрибутивная решётка А с операторами из специального множества Е изоморфна решётке О(V(А)) открыто-замкнутых порядковых фильтров на В (А). Изоморфизм / : А —> О (Б (А)) задаётся как <

/(х) = {Р:Р — открыто-замкнутый порядковый фильтр на А, и х е Р}.

Правило бинарной резолюции на основе дуальности Пристли выглядит следующим образом (ср. [17], следствия 5 и 6):

Из посылок (\~а]Ь1) V Сх ([^Ь1) V С2 выводится СХУС2 при условии, что ос, /3 £ 0{А) и а ^ /3,

где запись [а]Ь1 (или [а\Ь?) обозначает, что многозначный литерал Ь (т.е. элементарная формула многозначной логики с отрицаниями или без) общезначим (соответственно, опровержим) на множестве истинностных значений а; С\ и С'1 суть дизъюнкции литералов с метками вида [~оГ|; О (А) есть множество всех главных фильтров на алгебре истинностных значений А рассматриваемой логики, упорядоченное по включению. Для ясности изложения мы предполагаем, что Ь, С\ и С2 уже унифицированы. Заметим, что упомянутое правило резолюции по сути своей остаётся классическим (ср., например, [7]), изменения касаются только структуры литералов.

Мы доказываем следующую теорему о методе резолю- '

ций на основе теоремы Пристли и о логиках Лукасевича:

Теорема (Корректность метода резолюций). Пусть Ь — это произвольная логика Лукасевича, тогда метод резолюций на основе дуальности Пристли корректен относительно Ь, е.т.е. Ь конечнозначна.

Также мы получаем следующий результат:

Теорема (Критерий применимости метода резолюций) . Метод резолюций на основе теоремы представления Пристли корректен относительно произвольной многозначной логики, если и только если многообразие V, порождённое её алгеброй А истинностных значений, замкнуто относительно канонических расширений, т.е. для всех А € V верно, что 0(£)(А)) € V.

В седьмой главе — «Эффективное доказательство теорем в логиках Лукасевича» приводятся некоторые оптимизационные методы доказательства теорем в логиках Лукасевича. В частности, для бесконечнозначной логики Лукасевича Ьк0 даётся метод (см. [12]), основанный на теореме Мак-Нотона [6].

Теорема Мак-Нотона установила связь между множеством функций, определённых на п-мерном единичном кубе, и формулами с п различными переменными. Приведём несколько определений.

Определение. Пусть А — это формула Ьц0, а / — это п-местная действительная функция. Формула А представляет функцию / (или функция / представляется формулой А), если и только если

1. А содержит в точности п различных пропозициональных переменных,

2. / определена на интервале [0,1] и

3. для любых элементов х\,...,хп интервала [0,1] и любой функции присваивания значений V, такой что у(рг) = хг при 1 ^ г ^ п, выполняется условие

/(Х1,...,хп) =

Определение. Действительная функция /а(х\,...,хп) называется функцией приписывания значений формулы А(Рх,..., Рп) логики Ьц0, если верно, что

1. если А - Рг, тогда /А = Х{,

2. если А = В, тогда /д = 1 — /в,

3. если А = В —»• С, тогда

'1, если ¡в(х1,...,хп) ^

т-л = 1 , , ч , , , ч

1 - М^Ъ ■ ■ • , ®п) + • • • ,

в остальных случаях.

Теорема. Если А(Рг,..., Рп) — формула ЬКо, то А представляет её функцию приписывания значений , • • •,

Теорема (Мак-Нотон). Если А — это формула Ьн0, тогда её функция приписывания значений /д удовлетворяет следующим условиям:

1. /л непрерывна над [0,1]" и 1п^(/д) С [0,1];

2. область определения, [0,1]", подразделяется на коночное число т подобластей Юг, 1 ^ ? ^ т, это деление исчерпывающее и внутренние части подобластей не пересекаются;

3. существует т многочленов д\,---,дт вида

дг = аг,о + Ч-----1- аг<пхп.

где все а^ (1 ^ г ^ гп, 0 ^ ] ^ п) — это неотрицательные целые, такие что если (х15..., хп) €

А, то

IА (я- 1 ? • • ■ ) Д-п) = ) • • • » З'п)-

Задача проверки формулы Л на общезначимость требует определения того, принимает ли функция /д значение 1 надо всей её областью определения. А эта задача, в свою очередь, сводится к установлению, принимает ли каждая функция из /ь...,/ш значение 1 над всей той частью области определения, на которой она определяет /а- Совершенно закономерно, область определения Б разделяется на подобласти £>!,..., Вт , где /, определяет /д на Д. Приводятся некоторые таблицы и диаграммы, иллюстрирующие сокращённый метод проверки формулы логики Ьк0 на общезначимость.

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

с оператором резидуации, т.е. для нечёткозначных логик (включая логики Лукасевича) и релевантных логик.

В приложении доказывается вложимость произвольного пропозиционального немодального гильбертовского исчисления в исчисление резолюций с одноместными предикатами и приводится пример, иллюстрирующий подобное вложение: доказательство рефлексивности импликации в аксиоматической системе {В, С, W, Кь Х3}, рассмотренной в [3], с помощью программы автоматического поиска доказательства теорем OTTER. Таким образом доказано, что данная система аксиом является аксиоматизацией импликативного фрагмента классической логики высказываний.

Литература

[1] О. М. Аншаков и С. В. Рычков. О многозначных логических исчислениях // Семиотика и информатика, 19:90-117, 1982.

[2] Д. А. Бочвар и В. К. Финн. О многозначных логиках, допускающих формализацию анализа антиномий I // Исследования по математической лингвистике, математической логике и информационным языкам, стр. 238-295. М.: Наука, 1972.

[3] А. С. Карпенко. Многозначные логики, Вып. 4 из серии Логика и компьютер. М.: Наука, 1997.

[4] А. С. Карпенко. Характеризация классов натуральных чисел посредством логических матриц / / Труды

семинара логического центра ИФ РАН, Вып. XIV, стр. 217-225. М.: ИФРАН, 1999.

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

[6] Р. Мак-Нотон. Теорема о бесконечнозначной логике высказываний // Кибернетический сборник, 3, 1961.

[7] Ч. Чень и Р. Ли. Математическая логика и автоматическое доказательство теорем. М.: Мир, 1983.

[8] Ю. И. Янов и А. А. Мучник. О существовании к-значных замкнутых классов, не имеющих базиса // Доклады АН СССР, 127(1):44-46, 1959.

[9] S. Aguzzoli и A. Ciabattoni. Finiteness in infinite-valued logic // Journal of Logic, Language and Information, 9(1):5—29, 2000.

[10] M. Baaz и С. G. Fermuller. Resolution based theorem proving for many-valued logics // Journal of Symbolic Computation, 19(4):353-391, 1995.

[11] M. Baaz, C. G. Fermuller, G. Salzer, и R. Zach. Labeled calculi and finite-valued logics // Studia Logica, 61:7-33, 1998.

[12] G. Beavers. Automated theorem proving for Lukasiewicz logics // Studia Logica, 52(2):183-196, 1993.

[13] С. С. Chang. Algebraic analysis of many valued logics // Trans. Amer. Math. Soc., 88:467-490, 1958.

[14] R. L. O. Cignoli, I. M. L. D'Ottaviano, и D. Mundici. Algebraic foundations of many-valued reasoning, Вып. 7 из серии Trends in logic. Kluwer, Dordrecht, 1999.

[15] G. Rousseau. Sequents in many-valued logic I // Fundamenta Mathematicae, LX:23-33, 1967.

[16] V. Sofronie-Stokkermans. Duality and canonical extensions of bounded distributive lattices with operators, and applications to the semantics of non-classical logics I // Studia Logica, 64(1):93-132, 2000.

[17] V. Sofronie-Stokkermans. Automated theorem proving by resolution for finitely-valued logics based on distributive lattices with operators // Multiple-Valued Logic -An International Journal, 5(4):289-344, 2001.

[18] V. Sofronie-Stokkermans. Representation theorems and the semantics of non-classical logics, and applications to automated theorem proving // Beyond Two: Theory and Applications of Multiple Valued Logic. Редакторы M. Fitting и E. Orlowska, Studies in Fuzziness and Soft Computing, стр. 59-100. Springer, 2003.

Публикации автора по теме диссертации

[Г] В. Е. Комендантский. 3-значные изоморфы классической логики // Современная логика: проблемы

теории, истории и применения в науке. Материалы VI Общероссийской научной конференции, стр. 199200. СПбГУ, Июнь 2000.

[2'] В. Е. Комендантский. Незнание в логиках знания // Смирновские чтения. III международная конференция,, стр. 135-136. М.: ИФ РАН, Май 2001.

[3'] В. Е. Комендантский. Otter и доказательство рефлексивности импликации // Труды семинара логического центра ИФ РАН, Вып. XV, стр. 57-60. М.: ИФ РАН, 2001.

[4'] В. Е. Комендантский. Об игровой семантике бесконеч-нозначной логики Лукасевича // Современная логика: проблемы теории, истории и применения в науке. Материалы VII Общероссийской научной конференции, стр. 245. СПбГУ, Июнь 2002.

[5'] В. Е. Комендантский. Метод резолюций в смешанной логике Поста // Труды семинара логического центра ИФ РАН, Вып. XVI, стр. 64-74. М.: ИФ РАН, 2002.

[6'] В. Е. Комендантский. Теорема представления Пристли и метод резолюций в многозначных логиках // Логические исследования, Вып. 10. М.: Наука, 2003. В печати.

[7'] V. Ye. Komendantsky. Resolution for mixed Post logic // Proc. 4th ESSLLI Student Session, Trento, August 2002. University of Trento.

[8'] V. Ye. Komendantsky. On automated theorem proving by means of representation theory in Lukasiewicz logics // Smirnov's Readings. 4th International Conference, стр. 78-79, Moscow, May 2003. IPhRAS.

■

РНБ Русский фонд

2005-4 12775

Подписано в печать 18.09.2003. Зак. №001. Объём 0,84 уч.изд.л., 1,56 печ.л. Тир. 100 экз. Отпечатано на принтере сектора логики ИФРАН, Москва, Волхонка 14.

0 3 ОМ >'''03

Оглавление научной работы автор диссертации — кандидата философских наук Комендантский, Владимир Евгеньевич

Введение

1 Истинностно-функциональные семантики

§1 Семантика голосования.

§2 Переранд омизирующая семантика.

§3 Семантика сходства.

§4 Семантика рисков, или диалоговая семантика.

§5 Семантика допустимости.

§6 Рассуждения в теории меры.

§7 Семантика приближений.

§8 Импликация

§9 Отрицание.

2 Формализация многозначных логик

§1 Логика высказываний.

§2 Логика первого порядка.

§3 Алгебра.

§4 Вывод.

§5 Логика отмеченных формул.

§6 Секвенциальные и табличные исчисления

§7 Резолюция

3 Функциональный анализ многозначных логик

§1 Основные понятия.

§2 Критерии полноты и 5-полноты.

§3 Предикатная характеризация ^-замкнутых классов.

4 Метод резолюций для смешанной логики Поста

§1 Смешанная логика Поста PostL.

§2 Резолюция для PostL.

§3 Замечания

5 Теорема Чена

§1 Идеалы, отношения конгруэнтности и проблема представления

§2 Линейно упорядоченные MV-алгебры.

§3 Упорядоченная абелева группа G[c].

§4 Применение к бесконечнозначной логике Лукасевича.

6 Метод резолюций на основе теоремы представления дистрибутивных решёток с операторами

§1 Дуальность по Пристли.

§2 Модели, основанные на дуале Пристли.

§3 Автоматическое доказательство теорем.

§4 Канонические расширения.

7 Эффективное доказательство теорем в логиках Лукасевича

§1 Логика Лукасевича и линейная алгебра.

§2 Первый метод проверки общезначимости.

§3 Второй метод.

Введение диссертации2003 год, автореферат по философии, Комендантский, Владимир Евгеньевич

Многозначные логики появились в 20-х годах XX века в работах Поста и Лукасевича. Несколько позднее было предложено ещё несколько многозначных логик, таких как логика Бочвара, логики Гёделя, логика Клини. Интересный библиографический экскурс в многозначные логики можно найти в [7]. Изобретение этих логик было мотивировано разными задачами. Так, Лукасевич и Бочвар исходили из философских предпосылок, вводя третье значение в свои логики для формализации неполного или противоречивого знания; Пост и Гёдель руководствовались более техническими соображениями, когда обобщали классическую логику в n-значных системах; Клини же просто искал удобный формализм для анализа понятия частично определённой рекурсивной функции. Однако все эти логики объединяет важная отличительная особенность: в них ме-татеоретически заложена концепция, которую называют истинностной функциональностью. Согласно ей, всякое высказывание имеет некоторое значение истинности, и это значение может быть однозначно вычислено некоторой заранее определённой функцией по значениям входящих в это высказывание подвысказываний. Так, в случае конъюнкции А А Б высказываний А и В искомой функцией будет некоторая функция /д от значения А и значения В.

Если логика истинностно-функциональна, это непосредственно означает существование метода вычисления значения истинности для любого высказывания, записанного на языке этой логики. В этом состоит привлекательная в техническом смысле сторона многозначных логик: по любой формуле можно легко сказать, что она «значит». Сохраняется ли эта привлекательяость многозначных логик в теории вывода? К сожалению, нет, поскольку с ростом числа истинностных значений растёт и то внимание, которое им приходится уделять, а в это время падает эффективность рассуждений.

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

Степень разработанности проблемы. В нашей стране было получено большое количество результатов в области многозначных логик. Среди них можно особо отметить следующие: вычисление Яблонским всех пред-полных классов функций для трехзначной логики Поста в 1954 году, а также нескольких классов для случая k ^ 4 значений в 1958 году; доказательство существования к-значных замкнутых классов функций, не имеющих конечного базиса, для к > 2, найденное Яновым и Мучником в 1959 году (см. [30]); определение функциональных свойств логик Лукасевича Финном [4] в 1970 году; получение метода аксиоматизации произвольных конечнозначных логик Аншаковым и Рычковым [1] в 1982 году; установление Карпенко [9] связи импликации Лукасевича с классами простых чисел в 1999 году; построение Косовским и Тишковым [17] секвенциальных исчислений для классов конечнозначных логик в 2000 году. Также можно указать оригинальное доказательство полноты бесконечнозначной логики Лукасевича относительно реляционных семан-тик с тернарным отношением достижимости, полученное Васюковым в [88]. За рубежом многозначная логика в наше время является сложной разветвлённой отраслью науки. Многие работы общетеоретического характера публикуются не отдельными авторами, а коллективами авторов, например, статья по секвенциальным исчислениям с метками для конечнозначных логик [36] или монография по алгебраическим основаниям многозначных логик [46].

Актуальность темы диссертации. Сегодня для бесконечнозначных логик не существует хорошо обоснованной теории доказательств, хотя для конечнозначных логик табличные исчисления без сечений были построены ещё Руссо [80] в 1967 году. Некоторые исчисления для бесконечнозначных логик Лукасевича всё же определяются в литературе, например, Агуц-цоли и Чиабаттони [31] в 2000 году строят секвенциальное исчисление для бесконечнозначной логики, опирающееся на идею Мундичи о сводимо-^ сти проблемы разрешимости с бесконечнозначной логики на подходящий класс конечнозначных логик, и, следовательно, основанное на исчислениях для конечнозначных логик. В 2001 году Софрони-Стоккерманс [85] :' предложила метод доказательства теорем для большого класса многознач

Г - . ных логик, основанный на теореме представления алгебр истинностных значений. Кроме своей эффективности, этот метод интересен ещё и тем, что в нём посредством структур Крипке устанавливается соответствие между многозначными и модальными логиками. К сожалению, метод [85] неприменим к ряду широко распространённых бесконечнозначных логик. Данный метод исследован в диссертации, и на основе этого исследования w сделан вывод о возможности его обобщения на класс бесконечнозначных логик на основе подходящей теоремы представления алгебр истинностных значений.

Методы исследования. В работе используется логическая техника, как традиционная, например, секвенциальные логические исчисления, так и нетрадиционная: исчисления с «отмеченными формулами», S-классификация замкнутых классов функций многозначных логик, дуальные многозначным семантикам топологические модели. Автором работы вводится оригинальный метод на основе исчисления резолюций для доказательства теорем в многозначных логиках с линейно упорядоченными множествами истинностных значений.

Заключение научной работыдиссертация на тему "Теория вывода в многозначных логиках"

Основные результаты работы и положения, выносимые на защиту:

• В главе 4 получено корректное исчисление резолюций для всего класса конечнозначных логик Поста. Этот метод служит схемой для создания аналогичных методов для других классов конечнозначных логик с линейно упорядоченными множествами истинностных значений. В теореме 4.3 доказана корректность данного исчисления, в доказательстве использовались лемма об основных дизъюнкциях литералов 4.1 и лемма подъёма 4.2.

• В главе 6 в теоремах 6.11 и 6.12 получены результаты о мощности и границах применимости резолютивных методов поиска доказательства теорем на основе теорем представления к первопоряд-ковым многозначным логикам. В доказательстве этих результатов использовались теоремы Герке—Пристли 6.9 и 6.10 о незамкнутости бесконечно порождённых многообразий MV-алгебр относительно канонических расширений, теоремы Софрони 6.1, 6.2 и 6.7 и теорема Чена 5.20 о полноте бесконечнозначной логики Лукасевича относительно MV-алгебр.

Научная новизна работы состоит в том, что в ней

• предпринята попытка целостного философского анализа феномена символических систем многозначных логик;

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

Практическая значимость работы следует из прикладного характера той области, в которой проводится диссертационное исследование. С самого возникновения многозначные логики имели ясные семантики. Благодаря лёгкости задания интерпретаций и большому количеству разнообразных интерпретаций многозначные логики давно используются не только в академической деятельности, но и в промышленности и производстве. Они имеют множество инженерных приложений, а также они применимы в программировании задач из разных сфер практической деятельности. Теоретическая база, заложенная в диссертации, является необходимым условием для создания эффективных приложений на основе многозначных логик и внедрения этих приложений в производственные сферы. Особенного внимания с точки зрения практической значимости заслуживают результаты о бесконечнозначной логике Лука-севича. На основе этой логики строятся многие из т.н. нечётких логик, имеющих приложения в разнообразных задачах управления, например, в задачах управления сложными процессами, не имеющими простых математических моделей, таких как нелинейные процессы, а также в задачах обработки баз знаний, сформированных языковыми данными, полученными от экспертов. Приведём для наглядности некоторые промышленные реализации систем управления на основе нечётких логик: производство полупроводников (Canon), оптимизирование автобусных расписаний (Toshiba), система архивации документов (Mitsubishi Electric), система раннего предсказания землетрясений (Ин-т сейсмологии, Япония), диагностика раковых заболеваний (Kawasaki), распознавание написанных от руки текстов карманными компьютерами (Sony), однокнопочная система управления для стиральных машин (Matsushita, Hitachi), ядерные реакторы повышенной безопасности (Hitachi, Bernard), симуляция судебных разбирательств (ун-т г. Нагоя, Япония).

Апробация работы. Результаты работы докладывались автором на заседаниях научно-исследовательского семинара логического центра ИФ РАН, а также на следующих научных конференциях:

• Смирновские чтения 3, сектор логики ИФ РАН, 2001 г.;

• Современная логика: проблемы теории, истории и применения в науке, СПбГУ, 2002 г.;

• 14th European Summer School for Logic, Language and Information, Тренто, Италия, 2002 г.;

• Смирновские чтения 4, сектор логики ИФ РАН, 2003 г.;

• Summer School and Workshop on Proof Theory, Computation and Complexity, Дрезден, Германия, 2003 г.

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

1. Найти альтернативные естественные истинностно-функциональные семантики n-значных логик Поста.

2. Построить классификации 5-предполных классов связок известных многозначных логик.

3. Найти точную сложностную меру метода резолюций для смешанной логики Поста, предложенного в главе 4.

4. Построить аналогичный метод резолюций для смешанной логики Лукасевича.

5. Реализовать метод автоматического поиска доказательств теорем смешанных логик в компьютерной программе.

6. Доказать полноту суперлукасевичевой логики Ls относительно непредставимой алгебры Чена С.

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

8. Построить внутреннее исчисление (т.е. без отмеченных формул) для нечётких и релевантных логик.

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

Благодарности. Я выражаю свою глубочайшую признательность моим родителям Евгению Петровичу и Зое Владимировне Комендантским, оказывавшим мне поддержку во время написания этой диссертации. Хочу поблагодарить коллектив сектора логики ИФ РАН за предложения по улучшению текста диссертации, а также рецензента, оставшегося анонимным, за внесение поправок в рассуждения главы 4.

Заключение

Список научной литературыКомендантский, Владимир Евгеньевич, диссертация по теме "Логика"

1. О. М. Аншаков и С. В. Рынков. О многозначных логических исчислениях // Семиотика и информатика, 19:90-117, 1982.

2. Н. Белнап. Как нужно рассуждать компьютеру // Н. Белнап, Т. Стил. Логика вопросов и ответов, стр. 208-239. М., 1981.

3. Г. Биркгоф. Теория решёток. М.: Наука, 1984.

4. Д. А. Бочвар и В. К. Финн. О многозначных логиках, допускающих формализацию анализа антиномий I // Исследования по математической лингвистике, математической логике и информационным языкамстр. 238-295. М.: Наука, 1972.

5. Э. Б. Винберг. Курс алгебры. М.: Факториал-Пресс, 2001.

6. А. С. Карпенко. Фактор-семантика для бесконечнозначной логики Лукасевича // Неклассические логики, стр. 20-26. М.: ИФАН, 1985.

7. А. С. Карпенко. Многозначные логики, Вып. 4 из серии Логика и компьютер. М.: Наука, 1997.

8. А. С. Карпенко. Классификация пропозициональных логик // Логические исследования, Вып. 4, стр. 107-133. М.: Наука, 1997.

9. А. С. Карпенко. Характеризация классов натуральных чисел посредством логических матриц // Труды семинара логического центра ИФ РАН, Вып. XIV, стр. 217-225. М.: ИФРАН, 1999.

10. В. Е. Комендантский. 3-значные изоморфы классической логики // Современная логика: проблемы теории, истории и применения в науке. Материалы VI Общероссийской научной конференции, стр. 199-200. СПбГУ, Июнь 2000.

11. В. Е. Комендантский. Незнание в логиках знания // Смирновские чтения. III международная конференция, стр. 135-136. М.: ИФ РАН, Май 2001.

12. В. Е. Комендантский. OTTER и доказательство рефлексивности импликации // Труды семинара логического центра ИФ РАН, Вып. XV, стр. 57-60. М.: ИФ РАН, 2001.

13. В. Е. Комендантский. Метод резолюций в смешанной логике Поста // Труды семинара логического центра ИФ РАН, Вып. XVI, стр. 64-74. М.: ИФ РАН, 2002.

14. В. Е. Комендантский. Об игровой семантике бесконечнозначной логики Лукасевича // Современная логика: проблемы теории, истории и применения в науке. Материалы VII Общероссийской научной конференции, стр. 245. СПбГУ, Июнь 2002.

15. В. Е. Комендантский. Теорема представления Пристли и метод резолюций в многозначных логиках / / Логические исследования, Вып. 10. М.: Наука, 2003. В печати.

16. П. Кон. Универсальная алгебра. М.: Мир, 1968.

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

18. Я. Лукасевич. Аристотелевская силлогистика с точки зрения современной формальной логики. М. ИЛ, 1959.

19. Р. Мак-Нотон. Теорема о бесконечнозначной логике высказываний // Кибернетический сборник, 3, 1961.

20. С. С. Марченков. S-классификация функций многозначной логики // Дискретная математика, 9(3):125—152, 1997.

21. С. С. Марченков. Замкнутые классы булевых функций. М.: Наука, 2000.

22. С. С. Марченков. S-классификация функций трёхзначной логики. М.: Физматлит, 2001.

23. А. А. Набёбин. Логика и Пролог а дискретной математике. М.: МЭИ, 1996.

24. Нгуен Ван Хоа. О структуре самодвойственных замкнутых классов трёхзначной логики Рз // Дискретная математика, 4(4):82-95,1992.

25. Е. Расёва и Р. Сикорский. Математика метаматематики. М.: Наука, 1972.

26. А. В. Чагров. Логика, не являющаяся ни конечно-значной, ни бесконечно-значной // Труды семинара логического центра ИФ РАН, Вып. XIV, стр. 59-67. М.: ИФ РАН, 2000.

27. Ч. Чень и Р. Ли. Математическая логика й автоматическое доказательство теорем. М.: Мир, 1983.

28. Л. Л. Эсакиа. Доказуемостные интерпретации интуиционистской логики // Логические исследования, Вып. 5, стр. 19-24. М.: Наука, 1998.

29. С. В. Яблонский. Введение в дискретную математику. М.: Наука, 1986.

30. Ю. И. Янов и А. А. Мучник. О существовании fc-значных замкнутых классов, не имеющих базиса // Доклады АН СССР, 127(1):44-46,1959.

31. S. Aguzzoli и A. Ciabattoni. Finiteness in infinite-valued logic // Journal of Logic, Language and Information, 9(l):5-29, 2000.

32. О. Anshakov и S. Rychkov. On finite-valued propositional logical calculi // Notre Dame Journal of Formal Logic, 36(4):606-629, 1994.

33. A. Avron. Natural 3-valued logics — characterization and proof theory // Journal of Symbolic Logic, 56(l):276-294, 1991.

34. М. Baaz и С. G. Fermiiller. Resolution based theorem proving for many-valued logics // Journal of Symbolic Computation, 19(4):353-391, 1995.

35. M. Baaz, C. G. Fermiiller, G. Salzer, и R. Zach. Labeled calculi and finite-valued logics // Studia Logica, 61:7-33, 1998.

36. G. Beavers. Automated theorem proving for Lukasiewicz logics // Studia Logica, 52(2):183-196, 1993.

37. N. D. Belnap. A useful four-valued logic /J Modern uses of multiple-valued logic. Редакторы J. M. Dunn и G Epstein, стр. 8-37. Reidel, Dordrecht, 1977.

38. A. D. C. Bennett, J. B. Paris, и A. Vencovska. A new criterion for comparing fuzzy logics for uncertain reasoning // Journal of Logic, Language, and Information, 9(l):31-63, 2000.

39. S. Burris и H. P. Sankappanavar. A course in universal algebra. The Millenium edition. 2000. Доступна в интернете.

40. С. Chang и R. С. Lee. Symbolic logic and mechanical theorem proving. Academic Press, 1973.

41. С. C. Chang. Algebraic analysis of many valued logics // Trans. Amer. Math. Soc., 88:467-490,1958.

42. J. Chazarain, A. Riscos, J.A. Alonso, и Б. Briales. Multivalued logic and Groebner bases with applications to modal logic / / Journal of Symbolic Computation, 11:181-194, 1991.

43. A. Ciabattoni, D. M. Gabbay, и N. Olivetti. Cut-free proof systems for logics of weak excluded middle // Soft Computing—A Fusion of Fouondations, Methodologies and Applications, 2(4):147-156, 1999.

44. R. Cignoli и D. Mundici. An elementary proof of Chang's completeness theorem for the infinite-valued calculus of Lukasiewicz // Studia Logica, 58:79-97, 1997.

45. R. L. O. Cignoli, I. M. L. D'Ottaviano, и D. Mundici. Algebraic foundations of many-valued reasoning, Вып. 7 из серии Trends in logic. Kluwer, Dordrecht, 1999.

46. R. Dyckhoff. A deterministic terminating sequent calculus for Godel-Dummett logic // Logic Journal of the IGPL, 7(3):319-326, 1999.

47. H. Ganzinger и V. Sofronie-Stokkermans. Chaining techniques for automated theorem proving in finitely-valued logics. // Proceedings of the 30th ISMVL, стр. 337-344, Portland, Oregon, May 2000. IEEE Computer Society, IEEE Computer Society Press.

48. M. Gehrke и J. Harding. Bounded lattice expansions // Journal of Algebra, 238:345-371, 2001.

49. M. Gehrke и H. A. Priestley. Non-canonicity of MY-algebras j j In Houston Journal of Mathematics, 2002. в печати.

50. G. Gentzen. Untersuchungen iiber das Logische SchlieBen // Mathematische Zeitschrift, 39:176-210, 405-431, 1935.

51. R. Giles. Lukasiewicz logic and fuzzy set theory j j International Journal of Man-Machine Studies, 8:313-327, 1976.

52. R. Giles. A utility-valued logic for decision making // International Journal of Approximate Reasoning, 2:113-141, 1988.

53. M. L. Ginsberg. Multi-valued logic // Computational Intelligence, 4(3), 1988.

54. R. Hahnle. Towards an efficient tableau proof procedure for multipple-valued logics // Selected papers from computer science logic, CSL '90, Heidelberg, Germany. Ред. E. Borger и др., Вып. 553 из серии LNCS, стр. 248-260. 1991.

55. R. Hahnle. Automated theorem proving in multiple-valued logics. International Series of Monographs on Computer Science. Oxford University Press, 1994.

56. R. Hahnle. Commodious axiomatization of quantifiers in multiple-valued logic // Proc. 26th International Symposium on Multiple- Valued Logics, стр. 118-123, Los Alamitos, May 1996. IEEE Press.

57. R. Hahnle. Tableaux for many-valued logics // Handbook of Tableau Methods. Ред. M. D'Agostino и др., стр. 529-580. Kluwer, Dordrecht, 1999.

58. P. H£jek. Metamathematics of fuzzy logic, Вып. 4 из серии Trends in Logic: Studia Logica Library. Kluwer, Dordrecht, 1998.

59. P. Hajek и J. Paris. A dialogue on fuzzy logic // Soft Computing—A Fusion of Foundations, l(l):3-5, 1997.

60. P. Halmos. Algebraic logic I. monadic Boolean algebras // Compositio Math., 12:217-249, 1955.

61. J. P. Hayes. Pseudo-Boolean logic circuits // IEEE Transactions on Computers, C-35(7):602-612, 1986.

62. E. Hisdal. Are grades of membership probabilities? // Fuzzy Sets and Systems, 25:325-348, 1988.

63. V. Ye. Komendantsky. Resolution for mixed Post logic // Proc. 4th ESSLLI Student Session, Trento, August 2002. University of Trento.

64. V. Ye. Komendantsky. On automated theorem proving by means of representation theory in Lukasiewicz logics // Smirnov's Readings. 4-th International Conference, стр. 78-79, Moscow, May 2003. IPhRAS.

65. J. Lawry. A voting mechanism for fuzzy logic // International Journal of Approximate Reasoning, 19:315-333, 1998.

66. J. Lukasiewicz. О logice tr6jwartosciowej // Ruch Filozoficzny, 5:169171, 1920.

67. D. Mundici. Satisfiability in many-valued sentential logic is NP-complete

68. Theoretical Computer Science, 52:145-153, 1987.

69. J. B. Paris. A semantics for fuzzy logic // Soft Computing, 1:143-147, 1997.

70. J. B. Paris. Semantics for fuzzy logic supporting truth functionality. //с

71. Discovering the world, with fuzzy logic. Ред. V. Novak, Вып. 57 из серии Stud. Fuzziness Soft Comput., стр. 82-104. Heidelberg: Physica-Verlag, 2000.

72. J. Pavelka. On fuzzy logic I: Many-valued rules of inference // Zeitschrift fiir mathematische Logik und Grundlagen der Matematik, 25:45-72, 1979.

73. J. Pavelka. On fuzzy logic II: Enriched residuated lattices and semantics of propositional calculi // Zeitschrift fiir mathematische Logik und Grundlagen der Matematik, 25:119-134, 1979.

74. J. Pavelka. On fuzzy logic III: Semantical completeness for some many-valued propositional calculi // Zeitschrift fiir mathematische Logik und Grundlagen der Matematik, 25:447-464, 1979.

75. W. A. Pogorzelski. The deduction theorem for Lukasiewicz many-valued propositional calculi // Studia Logica, 15:7-23, 1964.

76. E. L. Post. Introduction to a general theory of elementary propositions // American Journal of Mathematics, 43(4): 163-185, 1921.

77. E. L. Post. Two-valued iterative systems of mathematical logic, Выл. 5 из серии Annals of Math. Studies. Princeton Univ. Press, 1941.

78. A. Prijatelj. Bounded contraction and Gentzen-style formulation of Lukasiewicz logics // Studia Logica, 57(2-3)-.437-456, 1996.

79. F. P. Ramsey. Truth and probability // The foundations of mathematics and other logical essays, стр. 156-198. Routledge and Kegan Paul, London, 1931.

80. A. Rose и J. B. Rosser. Fragments of many-valued statement calculi // Transactions of the American Mathematical Society, 87:1-53, 1958.

81. G. Rousseau. Sequents in many-valued logic I // Fundamenta Mathematicae, LX:23-33, 1967.

82. E. H. Ruspini. On the semantics of fuzzy logic // International Journal of Approximate Reasoning, 5:45-88, 1991.

83. F. Schick. Dutch bookies and money pumps // Journal of Philosophy, 83:112-119, 1986.

84. V. Sofronie-Stokkermans. Duality and canonical extensions of bounded distributive lattices with operators, and applications to the semantics of non-classical logics I // Studia Logica, 64(1):93-132, 2000.

85. V. Sofronie-Stokkermans. Duality and canonical extensions of bounded distributive lattices with operators, and applications to the semantics of non-classical logics II // Studia Logica, 64(2):151-172, 2000.

86. V. Sofronie-Stokkermans. Automated theorem proving by resolution for finitely-valued logics based on distributive lattices with operators // Multiple-Valued Logic — An International Journal, 5(4)-.289-344, 2001.

87. A. Urquhart. Many-valued logic // Handbook of Philosophical Logic. Редакторы D. Gabbay и F. Guenthner, Вып. Ill: Alternatives in Classical Logic, глава 2, стр. 71-116. Reidel, Dordrecht, 1986.

88. V. L. Vasyukov. The completeness of the factor semantics for Lukasiewicz's infinite-valued logics // Studia Logica, 52:143-167, 1993.

89. R. Wdjcicki. Theory of logical calculi. Reidel, Dordrecht, 1988.