Сущность бесконечнозначной предикатной логики, имеющей связку (нечеткое неравенство), близкой к импликации Лукасевича. Анализ ряда свойств секвенциального исчисления, в том числе свойств, служащих основой для процедур автоматического поиска доказательств.
Аннотация к работе
Предикатная логика на основе секвенциального исчисления, предназначенная для моделирования непрерывных шкал В работе предлагается бесконечнозначная предикатная логика более выразительная, чем логика Лукасевича.Отметим, что ограниченность истинностных значений предиката влечет конечность истинностного значения любой формулы (в частности, формулы с кванторами). Назовем формулу общезначимой, если истинностное значение этой формулы неотрицательно во всякой интерпретации при любой оценке. Заметим, утверждение о том, что во всякой интерпретации при любой оценке формула принимает истинностные значения, не меньшие рационального числа , эквивалентно тому, что формула общезначима. Отметим также, что любую формулу-значной предикатной логики Лукасевича можно представить в виде формулы логики так, что во всякой интерпретации при любой оценке истинностные значения этих формул будут совпадать. Мы представляем секвенцию (она совпадает со своим сукцедентом) как конечный список формул логики , разделенных запятыми; некоторые формулы могут повторяться; порядок формул в списке не имеет значения.В работе предложена бесконечнозначная предикатная логика, имеющая связку (нечеткое неравенство), близкую к импликации Лукасевича, но вычислительно более эффективную. Расширение традиционных подходов Лукасевича и Заде с единичным отрезком истинностных значений так, что каждый предикат имеет свой собственный отрезок истинностных значений, позволяет удобно моделировать различные шкалы путем использования различных отрезков.
Введение
Интерес к многозначным (в особенности, бесконечнозначным) логикам объясняется (см. [Gottwald, 2001], [Hajek, 1998]) их разнообразными применениями, включающими представление неопределенных знаний, приблизительные рассуждения и формальные основания нечетких логик, восходящих к Заде. Нечеткие логики, в свою очередь, широко используются в промышленных системах нечеткого контроля.
Применение методов линейного программирования для распознавания аксиом рациональнозначной пропозициональной логики со связкой, представляющей сложение истинностных значений, было предложено в [Косовский, 1995]. Развитие работы [Косовский, 1995] для логик конечнозначных предикатов осуществлено в [Косовский и др., 2000]. В [Hahnle, 1994] для конечнозначных и бесконечнозначных пропозициональных логик Лукасевича задача закрытия ветви семантической таблицы сводится к задаче смешанного целочисленного программирования, которая является NP-полной (поэтому полиномиальный алгоритм для решения такой задачи не известен в настоящее время). Для доказательства теорем в бесконечнозначных пропозициональных логиках известны и другие подходы (см., например, [Aguzzoli et al., 2000]). Для классической двузначной предикатной логики в [Beckert et al., 1996] предложен подход, основанный на семантических таблицах и задаче 0-1 целочисленного программирования. Для бесконечнозначной предикатной логики Лукасевича известны лишь исчисления гильбертовского типа (см. [Gottwald, 2001], [Hajek, 1998]), не подходящие для автоматического поиска доказательств. Автоматизация поиска доказательств в бесконечнозначных предикатных логиках остается перспективной исследовательской задачей.
В данной работе предлагается бесконечнозначная предикатная логика более выразительная, чем логика Лукасевича (описание бесконечнозначной предикатной логики Лукасевича можно найти, например, в [Hajek, 1998]), и разрабатывается подход к автоматизации поиска доказательств в предлагаемой логике. Формулируется секвенциальное исчисление и приводятся некоторые свойства исчисления. Задача распознавания аксиом этого исчисления сводится к задаче линейного программирования и может быть решена с помощью полиномиального алгоритма.
1. Синтаксис и семантика
Неотъемлемой частью каждого предикатного символа (пропозициональной переменной) является замкнутый отрезок вещественных чисел , где , - рациональные числа, . Такой отрезок называется отрезком истинностных значений предикатного символа (пропозициональной переменной). Это, в частности, означает, что значения предиката, который может быть подставлен вместо предикатного символа, принадлежат отрезку истинностных значений этого предикатного символа.
Термом является предметная переменная и предметная константа.
Атомарной формулой является любое рациональное число, пропозициональная переменная и предикатный символ, за которым следует заключенный в скобки конечный список термов, разделенных запятыми.
Используются следующие логические символы: (конъюнкция), (дизъюнкция), (квантор всеобщности), (квантор существования), (нечеткое неравенство), (модератор), где - рациональное число.
Формула логики определяется следующим образом. Атомарная формула является формулой логики. Если и - формулы, - рациональное число, - предметная переменная, то , , , , , являются формулами .
Рассмотрим некоторую интерпретацию языка логики . (Интерпретация определяется обычным образом, см., например, [Колмогоров и др., 2004], с. 69-72; но отрезки истинностных значений предикатных символов и пропозициональных переменных фиксированы). Обозначим истинностное значение замкнутой формулы в данной интерпретации.
Положим по определению . Т.о., нечеткое неравенство является многозначной импликацией, близкой к импликации Лукасевича.
Далее, , , (т.е. умножается на ). Т.о., модератор реализует положительное или отрицательное увеличение или уменьшение истинностного значения формулы; модератор трактуется как отрицание.
Наконец, , . Отметим, что ограниченность истинностных значений предиката влечет конечность истинностного значения любой формулы (в частности, формулы с кванторами).
Назовем формулу общезначимой, если истинностное значение этой формулы неотрицательно во всякой интерпретации при любой оценке.
Заметим, утверждение о том, что во всякой интерпретации при любой оценке формула принимает истинностные значения, не меньшие рационального числа , эквивалентно тому, что формула общезначима.
Отметим также, что любую формулу -значной предикатной логики Лукасевича можно представить в виде формулы логики так, что во всякой интерпретации при любой оценке истинностные значения этих формул будут совпадать. Действительно, истинностные значения отрицания и импликации Лукасевича вычисляются следующим образом: и ; поэтому отрицание и импликация Лукасевича представляются в как и .
Мы представляем секвенцию (она совпадает со своим сукцедентом) как конечный список формул логики , разделенных запятыми; некоторые формулы могут повторяться; порядок формул в списке не имеет значения. Потребуем, чтобы всякая секвенция была чистой.
Секвенция представляется в виде формулы как дизъюнкция всех формул этой секвенции. Представлением пустой секвенции в виде формулы является отрицательное число .
Назовем секвенцию общезначимой, если ее представление в виде формулы является общезначимой формулой.
2.1 Правила вывода
Ниже и обозначают части некоторой формулы, так что (т.е. результат конкатенации цепочек символов , , ) является формулой для некоторой выделенной формулы .
Определим знак (положительный или отрицательный) вхождения связки в формулу. Подчеркнутое вхождение в формулу вида является положительным. Если подчеркнутое вхождение в формулу вида является положительным (соответственно, отрицательным), то подчеркнутое вхождение в формулу вида является отрицательным (соответственно, положительным), и подчеркнутое вхождение в формулу вида является положительным (соответственно, отрицательным). В других случаях знак вхождения не определен.
Там, где это необходимо, мы обозначаем положительное вхождение как , отрицательное вхождение как ; если знак вхождения не определен или не важен, мы используем . Например, , причем знак первого вхождения в эту формулу не определен.
Пусть , , - рациональные числа, такие что , - неотрицательное рациональное число, - отрицательное рациональное число; - список формул (может, пустой); , , - формулы; , - предметные переменные, - терм; - результат подстановки терма на место всех свободных вхождений предметной переменной в . Кванторные правила вывода имеют стандартные ограничения для вывода чистых секвенций (см., например, [Косовский и др., 2000]).
Используются правила вывода, отчасти аналогичные правилам вывода для двузначного безантецедентного секвенциального исчисления: , , , , , , , , .
Также используются следующие правила (некоторые правила с вхождением не приводятся изза ограничения на объем статьи; их легко восстановить, поскольку они «симметричны» приведенным здесь правилам с вхождением ): , , , , , , , , , , , , , , , , , , , , , , , .
Наконец, используются правила, полученные из всех упомянутых выше правил, в которые входит , кроме правила , путем удаления .
2.2 Аксиомы
Сначала определим каноническую цепь неравенств (КЦН) следующим образом. Формулы вида и (где - модератор, - атомарная формула) являются КЦН. Если и - КЦН, то является КЦН.
Пусть дана секвенция . Рассматривая секвенцию как список формул, удалим из все формулы, которые не являются КЦН; тогда полученная секвенция называется базовой подсеквенцией секвенции .
Секвенция называется аксиомой, если базовая подсеквенция этой секвенции общезначима.
Нетрудно показать, что базовая подсеквенция общезначима тогда и только тогда, когда система линейных неравенств, описанная ниже, несовместна. Такая система линейных неравенств строится из базовой подсеквенции следующим образом.
Каждая пропозициональная переменная (каждый предикатный символ со списком аргументов) базовой подсеквенции заменяется на уникальную рациональнозначную переменную (все вхождения одного и того же предикатного символа с одним и тем же списком аргументов заменяются одной и той же рациональнозначной переменной). Каждое выражение вида заменяется на . Пусть выражение соответствует формуле базовой подсеквенции при только что описанном преобразовании. Тогда для каждой формулы базовой подсеквенции числовое неравенство включается в систему. Наконец, пусть рациональнозначная переменная соответствует пропозициональной переменной (предикатному символу со списком аргументов); тогда для каждой такой переменной , неравенства , , где - отрезок истинностных значений этой пропозициональной переменной (предикатного символа), включаются в систему.
Т.о., для проверки того, является ли секвенция аксиомой, требуется проверить несовместность соответствующей системы линейных неравенств (строгих и нестрогих) с рациональными коэффициентами над множеством всех рациональных чисел.
3. Некоторые свойства исчисления
Лемма 4.1. В исчислении все аксиомы общезначимы; заключение каждого правила вывода общезначимо, если посылки этого правила общезначимы; заключение каждого обращения каждого правила вывода общезначимо, если посылка этого обращения данного правила общезначима.
Теорема 4.2. (Семантическое обоснование исчисления) Если формула логики выводима в исчислении , то эта формула общезначима.
Предложение 4.3. (Непротиворечивость) Пустая секвенция не выводима в исчислении .
Лемма 4.4. Правило добавления допустимо в исчислении .
Теорема 4.5. Каждое правило вывода исчисления обратимо.
Рассмотрим классическую двузначную логику первого порядка со связками , , , кванторами , и истинностными константами (истина), (ложь). Безантецедентное секвенциальное исчисление для этой логики формулируется следующим образом. Правилами вывода являются все правила вывода из первого блока правил для , где в правилах , , , и заменены на , и удалены. Аксиомами являются секвенции видов: (a) ; (b) ; (c) ; где - атомарная формула.
Пусть - формула классической двузначной логики. Обозначим формулу логики , которая строится из следующим образом: каждое вхождение заменяется на , каждое вхождение заменяется на , каждое вхождение заменяется на модератор ; с каждым предикатным символом (пропозициональной переменной) ассоциируется отрезок истинностных значений .
Теорема 4.6. (Вложение двузначной логики) Формула выводима в исчислении тогда и только тогда, когда формула выводима в исчислении .
Теорема 4.8. Исчисление полно для пропозиционального фрагмента логики .
Правила вывода исчисления , содержащие неопределенный терм , назовем минус-правилами (по аналогии с подобными правилами секвенциального исчисления для классической двузначной логики, см. [Маслов и др., 1983]).
Главной проблемой при обратном поиске вывода (начиная с исходной формулы, для которой требуется построить вывод) в исчислении является нахождение термов для подстановки при контрприменениях (от заключений к посылкам) минус-правил. Таких термов для подстановки бесконечно много.
Для классической двузначной логики известны исчисления (см., например, [Кангер, 1967]), в которых устранен бесконечный перебор термов для подстановки при контрприменениях минус-правил. Мы сформулируем исчисление , обладающее таким свойством и равнообъемное исчислению .
Исчисление отличается от наличием дополнительного ограничения на минус-правила: терм может быть только одним из термов, которые входят в заключение правила и которые не являются связанными в заключении правила; если таких термов нет, то терм является какой угодно предметной переменной, не входящей в заключение правила.
Теорема 4.9. Для любой секвенции выводима в тогда и только тогда, когда выводима в .
В работе предложена бесконечнозначная предикатная логика, имеющая связку (нечеткое неравенство), близкую к импликации Лукасевича, но вычислительно более эффективную. Расширение традиционных подходов Лукасевича и Заде с единичным отрезком истинностных значений так, что каждый предикат имеет свой собственный отрезок истинностных значений, позволяет удобно моделировать различные шкалы путем использования различных отрезков. Язык логики Лукасевича расширен новой логической связкой - модератором, представляющим умножение формулы на рациональное число. Модераторы позволяют формализовать модификаторы типа «очень» эффективным способом; тогда как Заде применяет возведение функции принадлежности в квадрат для модификатора «очень», что усложняет вычисления и делает аксиоматизацию логики Заде более трудной. Также в данной работе предложено секвенциальное исчисление для введенной логики и доказан ряд свойств, облегчающих автоматический поиск вывода в этом исчислении.
Автор приносит глубокую благодарность профессору Косовскому Н.К. за внимание к этому исследованию и ценные советы.
Список литературы
Aguzzoli S., Ciabattoni A. Finiteness in infinite-valued Lukasiewicz logic. // Journal of Logic, Language and Information. 2000. № 9.
Beckert B., Hahnle R. Deduction by combining semantic tableaux and integer programming. // Lecture Notes in Computer Science. 1996. № 1092.
Gottwald S. A treatise on many-valued logics. - Baldock: Research Studies Press, 2001.
Hahnle R. Many-valued logic and mixed integer programming. // Annals of Mathematics and Artificial Intelligence. 1994. № 12.
Hajek P. Metamathematics of fuzzy logic. - Dordrecht: Kluwer Academic Publishers, 1998.
Кангер С. Упрощенный метод доказательства для элементарной логики. // Математическая теория логического вывода. - М.: Наука, 1967.
Косовский Н.К., Тишков А.В. Логики конечнозначных предикатов на основе неравенств. - СПБ: Изд-во С.-Петерб. ун-та, 2000.
Маслов С.Ю., Минц Г.Е. Теория поиска вывода и обратный метод. // Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. - М.: Наука, 1983.