Логика - доступно для всех

  • Увеличить размер шрифта
  • Размер шрифта по умолчанию
  • Уменьшить размер шрифта

Опровержение методом резолюций.

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

                                                           SG.

Каждая формула множества S и формула ØG (отрицание целевой теоремы) независимо преобразуются в множества предложений. В полученном совокупном множестве предложений C отыскиваются резольвируемые предложения, к ним применяется правило резолюций и резольвента добавляется в множество до тех пор, пока не будет получено пустое предложение. При этом возможны три случая:

  1. Среди текущего множества предложений нет резольвируемых. Это означает, что теорема опровергнута, то есть формула G не выводима из множества формул S.
  2. В результате очередного применения правила резолюции получено пустое предложение. Это означает, что теорема доказана. то есть SG.

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

 

 

Случайная новость