Помощь студентам в учебе
Автоматический поиск натурального вывода в классической логике предикатов
|
Введение 3
Глава 1. Автоматический поиск натурального вывода: история вопроса 9
§ 1.1. Натуральный вывод как тип логического вывода 9
§ 1.2. История создания систем автоматического поиска вывода 16
§ 1.3. Автоматический поиск вывода в натуральном исчислении 23
Глава 2. Анализ системы натурального вывода BMV 28
§ 2.1. Формулировка системы BMV 28
§ 2.2. Семантическая непротиворечивость системы BMV 35
Глава 3. Алгоритм поиска вывода в системе BMV 43
§ 3.1. Изменение формулировки системы BMV 43
§ 3.2. Унификация 47
§ 3.3. Правила поиска вывода в системе BMV 53
§ 3.4. Описание алгоритма поиска вывода в системе BMV 60
Глава 4. Анализ алгоритма поиска вывода в системе BMV 81
§ 4.1. Семантическая непротиворечивость алгоритма 81
§ 4.2. Свойства алгоритма 85
§ 4.3. Семантическая полнота алгоритма 96
Заключение 102
Литература 106
Глава 1. Автоматический поиск натурального вывода: история вопроса 9
§ 1.1. Натуральный вывод как тип логического вывода 9
§ 1.2. История создания систем автоматического поиска вывода 16
§ 1.3. Автоматический поиск вывода в натуральном исчислении 23
Глава 2. Анализ системы натурального вывода BMV 28
§ 2.1. Формулировка системы BMV 28
§ 2.2. Семантическая непротиворечивость системы BMV 35
Глава 3. Алгоритм поиска вывода в системе BMV 43
§ 3.1. Изменение формулировки системы BMV 43
§ 3.2. Унификация 47
§ 3.3. Правила поиска вывода в системе BMV 53
§ 3.4. Описание алгоритма поиска вывода в системе BMV 60
Глава 4. Анализ алгоритма поиска вывода в системе BMV 81
§ 4.1. Семантическая непротиворечивость алгоритма 81
§ 4.2. Свойства алгоритма 85
§ 4.3. Семантическая полнота алгоритма 96
Заключение 102
Литература 106
Актуальность темы исследования. Проблема поиска логического вывода традиционно считается одной из центральной тем логики. Бурное развитие данной проблематики в XX веке стимулировали, с одной стороны, фундаментальные работы Г. Генцена и Ж. Эрбрана и, с другой, появление ЭВМ. Возможность использования ЭВМ в процессе поиска логического вывода привела к появлению проблематики автоматического (машинного) поиска логического вывода.
В настоящее время определяющим фактором при предпочтении одной логической системы перед другой становится наличие (автоматической) процедуры поиска вывода. Такие процедуры существенным образом облегчают нахождение логического вывода и активно используются в педагогической работе.
В свою очередь, эти процедуры являются объектом исследования и постоянно сравниваются между собою по степени сложности (вычислительные затраты на поиск вывода), гибкости (возможность адаптации к нескольким логическим системам), удобства (понятный интерфейс, возможность поиска вывода как от посылок к заключению, так и от заключения к посылкам) и т. д.
В диссертационном исследовании тема автоматического поиска логического вывода ограничивается поиском вывода в натуральном исчислении типа Куайна в классической логике предикатов.
Натуральные системы типа Куайна, в отличие от натуральных исчислений типа Генцена, содержат прямое правило удаления квантора существования. Как следствие, в натуральных системах типа Куайна между посылками и заключением не всегда имеет место отношение логического следования.
Основное внимание авторы программ автоматического поиска натурального вывода обычно уделяют исчислениям типа Генцена. Непрямое правило удаления квантора существования в таких исчислениях предполагает построение дополнительного подвывода, гарантирующего наличие отношение логического следования между посылками и заключением. Поскольку построение дополнительного подвывода приводит к усложнению вывода, удобнее, по нашему мнению, пользоваться прямым правилом удаления квантора существования, т. е. искать вывод в исчислениях типа Куайна.
3
Степень разработанности проблемы. Долгое время исследования в области автоматического поиска логического вывода были сосредоточены на поиске вывода с помощью метода резолюции, секвенциальных и аналитико-табличных типов логического вывода.
Наличие свойства подформульности (в выводе формулы используются только подформулы или отрицания подформул этой формулы), которое следует из теоремы Генцена об устранении сечения, существенно облегчает поиск вывода в данных исчислениях [Генцен].
С нашей точки зрения, перечисленные логические методы являются не более, чем методами проверки формул на общезначимость и выполнимость. В то же время, традиционно под логическим выводом подразумевается возможность выведения некоторой формулы из некоторого (возможно, пустого) множества посылок, что достигается только лишь в аксиоматических и натуральных исчислениях.
Исчисления последнего вида особенно интенсивно исследуются на предмет автоматического поиска в них вывода в конце 80-х - начале 90-х гг. ХХ века.
Так, Дж. Поллок [Pollock] предложил программу поиска натурального вывода OSCAR в классической логике предикатов (а также в некоторых неклассических логиках) с использованием сколемовских термов. Он показал, что OSCAR работает в 40 раз эффективнее программы OTTER [Pollock], основанной на методе резолюций. С другой стороны, круг логических проблем, которые решает OSCAR, шире, чем аналогичный круг для OTTER. Дж. Поллоком была выдвинута также гипотеза, что OSCAR обладает свойством семантической полноты, т.е. что OSCAR может найти вывод любой общезначимой формулы классической логики предикатов.
Д. Пеллетье [Pelletier] предложил программу поиска натурального вывода Thinker в классической логике предикатов (а также в некоторых неклассических логиках) с предикатом равенства. Показывается, что Thinker решает 75 тестовых проблем для произвольного алгоритма поиска вывода в классической логике предикатов с предикатом равенства. Thinker не обладает свойством семантической полноты, поскольку количество переменных, которые используются в выводе, заранее ограничено.
У. Сиг вместе с Дж. Бернсом [Sieg], [Sieg & Byrnes] предложили программу автоматического поиска натурального вывода CMU PT в классической логике (авторы
4
также рассматривают возможность обобщения программы на неклассические логики). Специфика данного алгоритма состоит в том, что натуральный вывод строится не прямым, а косвенным образом. Сначала строится вывод в т.н. промежуточном исчислении, а затем показывается, каким образом можно преобразовать вывод в промежуточном исчислении в натуральный вывод. Авторы показывают, что CMU PT обладает свойством семантической полноты.
Д. Ли [Li] предложил программу поиска натурального вывода ANDP в классической логике. Особенно подчеркивая прикладное значение ANDP, Д. Ли дает машинные доказательства некоторых известных проблем математической логики: проблемы остановки машины Тьюринга, проблемы зависимости некоторых аксиом в формализации проективной геометрии и др. Вопрос, обладает ли ANDP свойством семантической полноты, остается открытым.
В.А. Бочаров, А.Е. Болотов и А.Е. Горчаков [Болотов и др.] предложили алгоритм поиска натурального вывода Prover для классической логики предикатов. Спецификой Prover является поиск вывода в натуральных исчислениях типа Куайна с использованием абсолютно и относительно ограниченных переменных. В процессе поиска вывода Prover использует также сколемовские термы. Касаясь вопроса о семантической полноте для Prover, авторы предлагают пути решения данной проблемы. Однако доказательства данного факта для Prover предложено не было.
Группа исследователей под руководством Н.А. Шанина [Шанин и др.] предложила процедуру поиска натурального вывода типа Генцена в классической логике высказываний. Отличительной особенностью данной процедуры является поиск вывода в секвенциальном исчислении. Затем полученный вывод в секвенциальном исчислении перестраивается в натуральный вывод типа Генцена. Отмечая пионерский характер данной работы (она вышла в 1964 году), подчеркнем, что вопрос о семантической полноте процедуры авторами не ставился, поскольку в формулах, для которых требуется найти натуральный вывод, разрешается использовать не более трех пропозициональных переменных. В значительной степени на работы группы под руководством Н.А. Шанина опирается У. Сиг.
В настоящее время определяющим фактором при предпочтении одной логической системы перед другой становится наличие (автоматической) процедуры поиска вывода. Такие процедуры существенным образом облегчают нахождение логического вывода и активно используются в педагогической работе.
В свою очередь, эти процедуры являются объектом исследования и постоянно сравниваются между собою по степени сложности (вычислительные затраты на поиск вывода), гибкости (возможность адаптации к нескольким логическим системам), удобства (понятный интерфейс, возможность поиска вывода как от посылок к заключению, так и от заключения к посылкам) и т. д.
В диссертационном исследовании тема автоматического поиска логического вывода ограничивается поиском вывода в натуральном исчислении типа Куайна в классической логике предикатов.
Натуральные системы типа Куайна, в отличие от натуральных исчислений типа Генцена, содержат прямое правило удаления квантора существования. Как следствие, в натуральных системах типа Куайна между посылками и заключением не всегда имеет место отношение логического следования.
Основное внимание авторы программ автоматического поиска натурального вывода обычно уделяют исчислениям типа Генцена. Непрямое правило удаления квантора существования в таких исчислениях предполагает построение дополнительного подвывода, гарантирующего наличие отношение логического следования между посылками и заключением. Поскольку построение дополнительного подвывода приводит к усложнению вывода, удобнее, по нашему мнению, пользоваться прямым правилом удаления квантора существования, т. е. искать вывод в исчислениях типа Куайна.
3
Степень разработанности проблемы. Долгое время исследования в области автоматического поиска логического вывода были сосредоточены на поиске вывода с помощью метода резолюции, секвенциальных и аналитико-табличных типов логического вывода.
Наличие свойства подформульности (в выводе формулы используются только подформулы или отрицания подформул этой формулы), которое следует из теоремы Генцена об устранении сечения, существенно облегчает поиск вывода в данных исчислениях [Генцен].
С нашей точки зрения, перечисленные логические методы являются не более, чем методами проверки формул на общезначимость и выполнимость. В то же время, традиционно под логическим выводом подразумевается возможность выведения некоторой формулы из некоторого (возможно, пустого) множества посылок, что достигается только лишь в аксиоматических и натуральных исчислениях.
Исчисления последнего вида особенно интенсивно исследуются на предмет автоматического поиска в них вывода в конце 80-х - начале 90-х гг. ХХ века.
Так, Дж. Поллок [Pollock] предложил программу поиска натурального вывода OSCAR в классической логике предикатов (а также в некоторых неклассических логиках) с использованием сколемовских термов. Он показал, что OSCAR работает в 40 раз эффективнее программы OTTER [Pollock], основанной на методе резолюций. С другой стороны, круг логических проблем, которые решает OSCAR, шире, чем аналогичный круг для OTTER. Дж. Поллоком была выдвинута также гипотеза, что OSCAR обладает свойством семантической полноты, т.е. что OSCAR может найти вывод любой общезначимой формулы классической логики предикатов.
Д. Пеллетье [Pelletier] предложил программу поиска натурального вывода Thinker в классической логике предикатов (а также в некоторых неклассических логиках) с предикатом равенства. Показывается, что Thinker решает 75 тестовых проблем для произвольного алгоритма поиска вывода в классической логике предикатов с предикатом равенства. Thinker не обладает свойством семантической полноты, поскольку количество переменных, которые используются в выводе, заранее ограничено.
У. Сиг вместе с Дж. Бернсом [Sieg], [Sieg & Byrnes] предложили программу автоматического поиска натурального вывода CMU PT в классической логике (авторы
4
также рассматривают возможность обобщения программы на неклассические логики). Специфика данного алгоритма состоит в том, что натуральный вывод строится не прямым, а косвенным образом. Сначала строится вывод в т.н. промежуточном исчислении, а затем показывается, каким образом можно преобразовать вывод в промежуточном исчислении в натуральный вывод. Авторы показывают, что CMU PT обладает свойством семантической полноты.
Д. Ли [Li] предложил программу поиска натурального вывода ANDP в классической логике. Особенно подчеркивая прикладное значение ANDP, Д. Ли дает машинные доказательства некоторых известных проблем математической логики: проблемы остановки машины Тьюринга, проблемы зависимости некоторых аксиом в формализации проективной геометрии и др. Вопрос, обладает ли ANDP свойством семантической полноты, остается открытым.
В.А. Бочаров, А.Е. Болотов и А.Е. Горчаков [Болотов и др.] предложили алгоритм поиска натурального вывода Prover для классической логики предикатов. Спецификой Prover является поиск вывода в натуральных исчислениях типа Куайна с использованием абсолютно и относительно ограниченных переменных. В процессе поиска вывода Prover использует также сколемовские термы. Касаясь вопроса о семантической полноте для Prover, авторы предлагают пути решения данной проблемы. Однако доказательства данного факта для Prover предложено не было.
Группа исследователей под руководством Н.А. Шанина [Шанин и др.] предложила процедуру поиска натурального вывода типа Генцена в классической логике высказываний. Отличительной особенностью данной процедуры является поиск вывода в секвенциальном исчислении. Затем полученный вывод в секвенциальном исчислении перестраивается в натуральный вывод типа Генцена. Отмечая пионерский характер данной работы (она вышла в 1964 году), подчеркнем, что вопрос о семантической полноте процедуры авторами не ставился, поскольку в формулах, для которых требуется найти натуральный вывод, разрешается использовать не более трех пропозициональных переменных. В значительной степени на работы группы под руководством Н.А. Шанина опирается У. Сиг.
Диссертационное исследование посвящено автоматическому поиску натурального вывода типа Куайна в классической логике предикатов. Специфика данной системы натуральной вывода - наличие прямого правила удаления квантора существования и наличие абсолютно и относительно ограниченных переменных.
Отсюда следует, что в общем случае между посылками и заключением вывода не имеет место отношение логического следования, поскольку формулировка прямого правила удаления квантора существования позволяет от общезначимых посылок переходить к необщезначимым заключениям.
Для обеспечения корректности системы наряду с понятием вывода (доказательства) в системе (Определение 2.1.3) вводится понятие завершенного вывода (завершенного доказательства), т.е. такого вывода (доказательства), в неисключенные посылки и заключение которого не входит ни одна абсолютно ограниченная переменная данного вывода (доказательства).21
Относительно завершенного вывода (завершенного доказательства) в системе натурального вывода предлагается доказательство утверждения о семантической непротиворечивости (Теорема 2.2.4), т.е. в произвольном завершенном выводе (доказательстве) между посылками и заключением имеет место отношение логического следования. Таким образом, всякая формула, доказуемая в системе, общезначима.
Доказательство теоремы о семантической непротиворечивости системы опирается на предложенное У. Куайном доказательство теоремы о семантической непротиворечивости.
Отметим, что в системе У.Куайна (а значит, в предложенном им доказательстве теоремы о семантической непротиворечивости) существенным образом используется алфавитный порядок, заданный на множестве используемых в языке переменных.
Система BMV не предполагает наличие алфавитного порядка на множестве используемых в выводе переменных. Поэтому доказательство теоремы о семантической непротиворечивости системы натурального вывода, предложенное У. Куайном, не обобщается на систему BMV.
21 Определение 2.1.4.
102
В связи с этим вводится понятие пассивной переменной в BMV-выводе (доказательстве), т.е. такой абсолютно ограниченной переменной в BMV-выводе (доказательстве), которая не ограничивает относительно ни одну абсолютно ограниченную переменную данного BMV-вывода (доказательства).22
Показывается, что в произвольном алго-выводе всегда найдется пассивная переменная (Лемма 2.2.4).
Далее предлагается алгоритм поиска вывода в данном исчислении, который является модификацией алгоритма поиска натурального вывода, разработанного В. А. Бочаровым, А.Е. Болотовым и А.Е. Горчаковым.
С использованием теоремы о семантической непротиворечивости системы натурального вывода BMV показывается, что данный алгоритм обладает свойством семантической непротиворечивости, поскольку каждый вывод (доказательство), полученный алгоритмом, является выводом (доказательством) в системе BMV (Теорема 4.1.2).
Понятие вывода (доказательства) в системе BMV предполагает, что в выводе (доказательстве) ни одна переменная не ограничивает сама себя. Переменная ограничивает другую переменную согласно формулировкам правил V^ Зи.
Экспликация отношения ограничения показывает, что данное отношение, заданное на множестве переменных вывода (доказательства), обладает свойствами иррефлексивности (ни одна переменная не ограничивает сама себя) и транзитивности (если переменная x ограничивает переменную у и переменная у ограничивает z, то переменная x ограничивает переменную z).
Таким образом, отношение ограничения, заданное на множестве переменных вывода (доказательства), является отношением строгого (частичного) порядка.
В силу того, что теория строгого порядка разрешима, процедура проверки, ограничивает ли произвольная переменная сама себя, конечна для произвольного завершенного вывода (доказательства).
Встроенный в алгоритм поиска вывода стандартный алгоритм унификации адаптирован для работы с абсолютно и относительно ограниченными переменными и содержит вышеупомянутую процедуру поиска в выводе (доказательстве) переменной, которая ограничивает сама себя.
22 Определение 2.2.1.
103
Минимальной единицей алгоритмического вывода является блок - непустая, конечная последовательность формул. Последовательность блоков образует собой древовидную структуру - дерево поиска вывода, в котором переход от одного блока к другому осуществляется с помощью правил поиска вывода.
Показывается конечность ветвления для произвольного блока в произвольном дереве поиска вывода (Лемма 4.3.1).
Опираясь на представление алгоритмического натурального вывода в виде древовидной структуры, выделяется некоторая нить данного дерева, множество формул в которой образует множество Хинтикки (модельное множество).
Таким образом, если для некоторой выводимости формулы из (возможно, пустого) множества посылок невозможно построить алгоритмический вывод, то данная формула логически не следует из данного множества посылок и алгоритмический вывод содержит (возможно, бесконечную) контрмодель, т.е. такую интерпретацию, при которой все формулы из данного множества посылок принимают значение «истина», а данная формула принимает значение «ложь».
Отсюда следует по контрапозиции, что предложенный алгоритм поиска натурального вывода типа Куайна в классической логике предикатов первого порядка обладает свойством семантической полноты, т.е. для любой общезначимой формулы классической логики предикатов можно построить вывод в предложенном алгоритме (Теорема 4.3.7).
Поскольку всякий алгоритмический вывод есть вывод в системе BMV, из утверждения о семантической полноте алгоритма следует утверждение о семантической полноте системы BMV (Теорема 4.3.8).
Отсюда следует, что в общем случае между посылками и заключением вывода не имеет место отношение логического следования, поскольку формулировка прямого правила удаления квантора существования позволяет от общезначимых посылок переходить к необщезначимым заключениям.
Для обеспечения корректности системы наряду с понятием вывода (доказательства) в системе (Определение 2.1.3) вводится понятие завершенного вывода (завершенного доказательства), т.е. такого вывода (доказательства), в неисключенные посылки и заключение которого не входит ни одна абсолютно ограниченная переменная данного вывода (доказательства).21
Относительно завершенного вывода (завершенного доказательства) в системе натурального вывода предлагается доказательство утверждения о семантической непротиворечивости (Теорема 2.2.4), т.е. в произвольном завершенном выводе (доказательстве) между посылками и заключением имеет место отношение логического следования. Таким образом, всякая формула, доказуемая в системе, общезначима.
Доказательство теоремы о семантической непротиворечивости системы опирается на предложенное У. Куайном доказательство теоремы о семантической непротиворечивости.
Отметим, что в системе У.Куайна (а значит, в предложенном им доказательстве теоремы о семантической непротиворечивости) существенным образом используется алфавитный порядок, заданный на множестве используемых в языке переменных.
Система BMV не предполагает наличие алфавитного порядка на множестве используемых в выводе переменных. Поэтому доказательство теоремы о семантической непротиворечивости системы натурального вывода, предложенное У. Куайном, не обобщается на систему BMV.
21 Определение 2.1.4.
102
В связи с этим вводится понятие пассивной переменной в BMV-выводе (доказательстве), т.е. такой абсолютно ограниченной переменной в BMV-выводе (доказательстве), которая не ограничивает относительно ни одну абсолютно ограниченную переменную данного BMV-вывода (доказательства).22
Показывается, что в произвольном алго-выводе всегда найдется пассивная переменная (Лемма 2.2.4).
Далее предлагается алгоритм поиска вывода в данном исчислении, который является модификацией алгоритма поиска натурального вывода, разработанного В. А. Бочаровым, А.Е. Болотовым и А.Е. Горчаковым.
С использованием теоремы о семантической непротиворечивости системы натурального вывода BMV показывается, что данный алгоритм обладает свойством семантической непротиворечивости, поскольку каждый вывод (доказательство), полученный алгоритмом, является выводом (доказательством) в системе BMV (Теорема 4.1.2).
Понятие вывода (доказательства) в системе BMV предполагает, что в выводе (доказательстве) ни одна переменная не ограничивает сама себя. Переменная ограничивает другую переменную согласно формулировкам правил V^ Зи.
Экспликация отношения ограничения показывает, что данное отношение, заданное на множестве переменных вывода (доказательства), обладает свойствами иррефлексивности (ни одна переменная не ограничивает сама себя) и транзитивности (если переменная x ограничивает переменную у и переменная у ограничивает z, то переменная x ограничивает переменную z).
Таким образом, отношение ограничения, заданное на множестве переменных вывода (доказательства), является отношением строгого (частичного) порядка.
В силу того, что теория строгого порядка разрешима, процедура проверки, ограничивает ли произвольная переменная сама себя, конечна для произвольного завершенного вывода (доказательства).
Встроенный в алгоритм поиска вывода стандартный алгоритм унификации адаптирован для работы с абсолютно и относительно ограниченными переменными и содержит вышеупомянутую процедуру поиска в выводе (доказательстве) переменной, которая ограничивает сама себя.
22 Определение 2.2.1.
103
Минимальной единицей алгоритмического вывода является блок - непустая, конечная последовательность формул. Последовательность блоков образует собой древовидную структуру - дерево поиска вывода, в котором переход от одного блока к другому осуществляется с помощью правил поиска вывода.
Показывается конечность ветвления для произвольного блока в произвольном дереве поиска вывода (Лемма 4.3.1).
Опираясь на представление алгоритмического натурального вывода в виде древовидной структуры, выделяется некоторая нить данного дерева, множество формул в которой образует множество Хинтикки (модельное множество).
Таким образом, если для некоторой выводимости формулы из (возможно, пустого) множества посылок невозможно построить алгоритмический вывод, то данная формула логически не следует из данного множества посылок и алгоритмический вывод содержит (возможно, бесконечную) контрмодель, т.е. такую интерпретацию, при которой все формулы из данного множества посылок принимают значение «истина», а данная формула принимает значение «ложь».
Отсюда следует по контрапозиции, что предложенный алгоритм поиска натурального вывода типа Куайна в классической логике предикатов первого порядка обладает свойством семантической полноты, т.е. для любой общезначимой формулы классической логики предикатов можно построить вывод в предложенном алгоритме (Теорема 4.3.7).
Поскольку всякий алгоритмический вывод есть вывод в системе BMV, из утверждения о семантической полноте алгоритма следует утверждение о семантической полноте системы BMV (Теорема 4.3.8).