Математическое введение в декларативное программирование. Зюзысов В.М. - 28 стр.

UptoLike

Составители: 

Классические методы доказательства
1. Использование теоремы о дедукции.
2. Доказательство импликаций с помощью контропозиции.
3. Доказательство с помощью противоречия (от противного).
4. Доказательство контпримером.
5. Метод математической индукции.
5.1 Использование теоремы о дедукции
Теорема о дедукции служит обоснованием следующего приема, который часто ис-
пользуют в математических доказательствах. Для того, чтобы доказать утверждение «Ес-
ли A, то B» предполагают, что справедливо A и доказывают справедливость B. Теорема о
дедукции справедлива для исчисления высказываний, но оказывается, что она остается в
силе и для теории первого порядка. Точнее, если формулы исчисления предикатов перво-
го порядка A и B замкнуты (тогда в любой интерпретации их истинность вполне опреде-
лена), то для этих формул справедливо утверждение теоремы о дедукции.
Пример. Докажите, что для каждого целого n, если n четное, то n
2
тоже четное.
Доказательство. Так как n четное, то его можно представить в виде n=2m, где m
целое число. Поэтому, n
2
= (2m)
2
= 4 m
2
= 2 (2 m
2
), где 2 m
2
целое число, т.е. n
2
четное.
5.2 Доказательство импликаций с помощью контропозиции
Рассмотрим условное высказывание вида AB, где Aконъюнкция посылок, B
заключение. Иногда удобнее вместо доказательства истинности этой импликации устано-
вить логическую истинность некоторого другого высказывания, равносильного исходно-
му. Такие формы доказательства называются косвенными методами доказательства.
Один из наиболее применяемый косвенный вид доказательстваэто доказательст-
во с помощью контропозиции.
Контропозицией формулы A B называется равносильная формула ¬В ¬A. По-
этому, если мы установим истинность контропозиции, то тем самым докажем истинность
исходной импликации.
Пример. На основе контропозиции докажите, что если m и nпроизвольные поло-
жительные целые числа такие, что m×n100, то либо m10, либо n10.
Доказательство. Контропозицией исходному утверждению служит следующее вы-
сказывание: «Если m>10 и n>10, то m×n>100», что очевидно.
Преимущества метода доказательства с помощью контропозиции проявляются при
автоматизированном способе доказательства, т.е. когда доказательство совершает компь-
ютер с помощью специальных программных систем доказательства теорем.
При построении выводов не всегда целесообразно ждать появления искомого за-
ключения, просто применяя правила вывода. Именно такое часто случается, когда мы де-
лаем допущение A для доказательства импликации A B. Мы применяем цепное правило
и модус поненс к A и другим посылкам, чтобы в конце получить B. Однако можно пойти
по неправильному пути, и тогда будет доказано много предложений, большинство из ко-
торых не имеет отношения к нашей цели. Этот метод носит название прямой волны и име-
ет тенденцию порождать лавину промежуточных результатов, если его запрограммиро-
вать для компьютера и не ограничить глубину.
Другая возможностьиспользовать контрапозицию и попытаться, например, дока-
зать ¬B ⊃¬A вместо A B. Тогда мы допустим ¬B и попробуем доказать ¬A. Это позво-
ляет двигаться как бы назад от конца к началу, применяя правила так, что старое заключе-
ние играет роль посылки. Такая организация поиска может лучше показать, какие
результаты имеют отношение к делу. Она называется поиском от цели.
28