<<
>>

1.3.Автоматический поиск вывода в натуральном исчислении

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

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

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

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

1) программа THINKER, разработанная Д. Пеллетье (J. Pelletier) [Pelletier];

2) программа OSCAR, разработанная Дж. Поллоком (J. Pollock) [Pollock];

3) программа ANDP (Automated Natural Deduction Prover), разработанная Д. Ли (D. Li) [Li];

4) программа CMU PT (Carnegie Mellon University Proof Tutor), разработанная У. Сигом (W. Sieg), Р. Шейнсом (R. Scheines) и Дж. Бернсом (J. Byrnes) [Sieg], [Sieg &Byrnes], [Byrnes];

5) программа Symlog (Symbolic Logic), разработанная Ф. Портораро (F. Portoraro) [Portoraro];

6) программа Prover, разработанная В.А. Бочаровым, А.Е. Болотовым и А.Е. Горчаковым и модифицированная В.О. Шангиным [Болотов и др.], [Болотов и др.1], [Шангин], [Bocharov et al].

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

1) алгоритм работает с предикатом равенства;

2) алгоритм работает с эквиваленцией;

3) алгоритм работает с неклассическими логиками;

4) множество используемых алгоритмом переменных ограничено;

5) для алгоритма доказываются теоремы о его свойствах (непротиворечивость, полнота и т.д.);

6) алгоритм использует сколемовские термы;

7) алгоритм имеет программную реализацию.

Значениями данной таблицы будут символы: + (признак имеется), - (признак

отсутствует) и +- (требует доработки).

Комментарий.

Из перечисленных программ только Thinker работает с предикатом равенства. Соответственно, среди предложенных программ только Thinker может построить вывод для всех 75 проблем, предложенных в [Pelleti er2], [Pelletier3]. Данный факт неудивителен, поскольку у Thinker и у списка 75 тестовых задач для алгоритма поиска вывода один и тот же автор - Д. Пеллетье.

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

Безусловным преимуществом алгоритма является возможность работы не только в классической, но и в неклассических логиках. Программа Thinker умеет работать в модальной логике [Pelletier]; программа Oscar - в логике «отменяемых» (defeasible) рассуждений; программа ANDP - в интуиционистской логике, и, наконец, можно рассматривать работы [Макаров], [Шангин1], [Шангин3] о поиске вывода в интуиционистской логике высказываний как перенесение идей Prover на интуиционистскую логику.

Только программа Thinker допускает ограничение (по умолчанию - 20) на количество переменных, которое можно использовать при построении вывода. По желанию пользователя, это количество может меняться. Однако наличие данного ограничения принципиально для поиска вывода. Если множество таких переменных

исчерпано (т.е. все n переменных использованы в выводе), то поиск вывода прекращается.

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

Строка «Свойства» отмечает разработанность метатеоретических проблем для данных алгоритмов. Например, «+-» столбце для Oscar и ANDP означает: доказано, что данные алгоритмы семантически непротиворечивы, т.

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

По разным причинам, метатеоретическая проблематика отсутствует для программ Thinker и Symlog. По словам Ф. Портораро, автора программы Symlog, «мы считаем вопрос о полноте алгоритма второстепенным: во-первых, он слишком далеко отстоит от темы нашего исследования; во-вторых, он не отвечает задачам алгоритма. Задача нашего алгоритма - предоставлять всестороннюю помощь при построении вывода, а не болезненно строить формальные выводы определенного вида. Поэтому вопрос о полноте нашего алгоритма отходит на второй план и вовсе исчезает тогда, когда алгоритм начинает оказывать помощь при работе с другими формальными системами, например, с арифметикой или теорией множеств» [Portoraro, с. 59].

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

Что касается Thinker, то данный алгоритм неполон, если учесть вышеуказанное ограничение на количество используемых в выводе переменных: «Очень трудно оценить семантическую полноту программы Thinker потому, что он может прийти к пункту J (остановка алгоритма) в различных случаях; в том числе и тогда, когда формула является логически общезначимой, Thinker может остановиться, потому что кончатся переменные» [Pelletier, с. 33]. С другой стороны, он пишет, что неясен ответ на вопрос, будет ли Thinker семантически полон, если данное ограничение на количество переменных будет снято.

Теорема о семантической полноте доказана для CMU PT. Предложенный У. Сигом метод (см. также [Sieg], [Sieg &Byrnes], [Byrnes]) заключается в том, что по дереву вывода, которое не является доказательством, можно построить контрмодель для данной формулы или для данной выводимости.

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

Не все алгоритмы используют в своей работе сколемизацию. Под сколемизацией здесь имеется ввиду явная сколемизация, т. е. добавление в язык логики предикатов особых свободных переменных и предметных функторов, с помощью которых образуется сколемовский терм. Сколемизация осуществляется в Oscar, CMU PT и Symlog.

Однако поиск вывод не обязательно предполагает явную сколемизацию. Существуют различные формы неявной сколемизации. Например, Thinker предполагает в процессе поиска вывода использовать т.н. «шаблоны» (templates), которые при окончательном построении вывода превращаются в формулы. Например, снятие V с формулы VxA(x, y) порождает шаблон A(@, y). Prover также использует неявную сколемизацию, о чем подробно говорится далее.

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

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

Однако здесь мы отметим те существенные различия, которые лежат между подходом У. Сига и нашим подходом.

Во-первых, в диссертационном исследовании исследуется система НВ с прямым правилом удаления 3 (в таких системах НВ заключение в общем случае не является логическим следствием из множества всех неисключенных посылок.) У. Сиг, в свою очередь, работает с системой НВ с непрямым правилом удаления 3.

Во-вторых, в диссертационном исследовании поиск вывода осуществляется непосредственно в системе НВ, а предложенный У. Сигом алгоритм CMU PT использует для поиска вывода промежуточные, вставочные исчисления (intercalation calculi). По внешнему виду такие исчисления напоминают секвенциальные исчисления. Вывод в таких исчислениях затем перестраивается в натуральный вывод.

Таким образом, мы вновь сталкиваемся с ситуацией, которая стимулировала развитие исследований именно по поиску натурального вывода: сначала вывод строится в другом исчислении (которое более благоприятно с точки зрения автоматического поиска вывода), а затем вывод в этом исчислении конструктивно перестраивается в натуральный вывод [Andrews]. Т.е. натуральный вывод в CMU PT строится не в системе натурального вывода, а с помощью промежуточного исчисления.

Что касается Prover, то программа строит натуральный вывод именно в системе натурального вывода. Таким образом, наша работа заполняет своеобразную лакуну, которая образовалась в области автоматического поиска НВ.

<< | >>
Источник: ШАНГИН ВАСИЛИЙ ОЛЕГОВИЧ. АВТОМАТИЧЕСКИЙ ПОИСК НАТУРАЛЬНОГО ВЫВОДА В КЛАССИЧЕСКОЙ ЛОГИКЕ ПРЕДИКАТОВ. Диссертация на соискание ученой степени кандидата философских наук. Москва - 2004. 2004

Еще по теме 1.3.Автоматический поиск вывода в натуральном исчислении:

  1. ШАНГИН ВАСИЛИЙ ОЛЕГОВИЧ. АВТОМАТИЧЕСКИЙ ПОИСК НАТУРАЛЬНОГО ВЫВОДА В КЛАССИЧЕСКОЙ ЛОГИКЕ ПРЕДИКАТОВ. Диссертация на соискание ученой степени кандидата философских наук. Москва - 2004, 2004
  2. Поиск определения воли
  3. В поиске мыслительного феномена повторения одинакового
  4. 2. Изложение учения ранних пифагорейцев: поиск источников концептов логики и зла
  5. Оглавление
  6. Эврит
  7. Оглавление
  8. Терминологические и методологические проблемы
  9. Другие примеры прото-упорядочивания
  10. Проблема интерпретации учения ранних пифагорейцев
  11. Введение
  12. Специфика доксографии и краткий обзор академического изучения раннего пифагореизма
  13. Стоицизм
  14. Проблемы изучения трактата
  15. Библиографический список использованной литературы
  16. Заключение
  17. Безволие — отступление перед реальностью
  18. ВВЕДЕНИЕ
  19. 2.1. Тимей Локрский. Биографические свидетельства