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

GD Star Rating
loading...

17 Responses to Теоремы системы автоматического доказательства

  1. Tuans:

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

  2. Zvin:

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

  3. Tuans:

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

  4. Zvin:

    но разве задачи не сводятся к «доказать, что предложенная нами расстановка знаков в выражении истинна»? Иными словами, например, я спрашиваю: дано выражение *^n+y^n=z^n; *,y,z,n — натуральные числа, n=2, может ли выполняться предложенное равенство? Программа отвечает что да, раскладывая её до базовых логических операций.

    Но чёрт её дери, стоит нам заменить условие с n=2 на n>2, и программа оказывается полностью бессильна.

  5. Tuans:

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

  6. Zvin:

    интересно, спасибо.

  7. Zvin:

    А можно ли такие системы использовать, чтобы доказывать хотя бы простенькие теоремы, исходя из других аксиоматических систем? Например, теоремы евклидовой геометрии из без–точечной геометрии Уайтхеда?

  8. Peels:

    Во–первых, задачи не все сводятся к утверждениям вида «доказать, что найдется». Есть еще «доказать, что не найдется», а это обычно на порядок сложнее.

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

    В–третьих, системы автоматического доказательства теорем вполне способны перебирать большие пространства утверждений и таким образом «доказывать» кучу всякого, только большинство из этого «всякого» не является чем–то очень нужным (доказательство промежуточного утверждения «5*20=100» или «найдется х такой что * + y — z > 0» может оказаться чем–то новым для машины, но абсолютно ненужным для нас), а пока они в своем переборе доберутся до чего–то полезного можно состариться.

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

  9. Zvin:

    почему эта область вышла из моды, как вы думаете? Уж очень заманчиво выглядят результаты, да и практические достижения есть.

  10. Peels:

    Потому что за 50 лет беспомощных разработок в области символьной логики обещанного искуственного интеллекта так и не родилось. В то же время стоило 10 лет попилить мат. статистику и анализ данных, как из компьютеров этот неожиданный интеллект забил ключом. В результате большинство людей, которые могли бы сейчас продолжать корпеть над символьными вычислениями, предпочтут более динамичную и интересную область датамайнинга. А в ней сейчас есть намного более возбуждающие области нежели доказательства теорем. Тренд примерно в духе «мы лучше научим компьютеры читать ваши мысли и захватим мир, нафиг нам эти ваши ненужные теоремы».

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

  11. SMDummy:

    тот результат, о котором вы говорите, называется теоремой Успенского–Райса(так можно договориться до того, что всё в логике Чёрч придумал, прямо как Коши в анализе:. Далее, я совершенно не вижу тут связи с возможностью доказывать теоремы. В фиксированной формальной системе для логики первого порядка любое верное утверждение имеет доказательство(по теореме Гёделя о полноте).
    Таким образом, просто перебирая все конечные строчки мы–таки получим доказательств(по строчке можно вычислить, доказательство оно или нет)

  12. Zvin:

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

  13. SMDummy:

    Большинство математиков к перспективе относятся очень скептически. Формализация любого НОРМАЛЬНОГО доказательства(не из начальных курсов по математике) формализуется крайне сложно в силу бесчисленного количества оговорок, и общих мест–стандартных рассуждений этой области, которые никто в не приводит. Вообще, мне кажется, нужно себя очень не любить, чтобы заниматься формализацией, топтаться на месте, вместо движения вперёд.

  14. SMDummy:

    что–то я заговариваюсь.

  15. Peels:

    У меня с именами плохо. Райс, да, более адекватное имя здесь, хотя на мой взгляд там из одного настолько вытекает второе, что без разниц. Про Успенского не слышал, забавно.

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

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

  16. SMDummy:

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

  17. Peels:

    А причем здесь ZFC и новые аксиомы?

    Арифметика входит в ZFC, поэтому ZFC неполна. Перебор доказательств — это хорошо, но для некоторых утверждений может не найтись доказательства и перебор окажется бесконечен.

Добавить комментарий