Принцип резолюции

Существует эффективный алгоритм логического вывода — алгоритм резолюции. Этот алгоритм основан на том, что выводимость формулы В из множества посылок F1; F2; F3; . . . Fn равносильна доказательству теоремы

|¾(F1&F2&F3&. . .&Fn®B),

формулу которой можно преобразовать так:

|¾(F1&F2&F3&. . .&Fn®B) =

|¾(ù(F1&F2&F3&. . .&Fn)ÚB) =

|¾ù(F1&F2&F3&. . .&Fn&( F2ù B)).

Следовательно, заключение В истинно тогда и только тогда, когда формула (F1&F2&F3&…&Fn&(ùB))=л. Это возможно при значении “л” хотя бы одной из подформул Fi илиùB.

 Для анализа этой формулы все подформулы Fi иùB должны быть приведены в конъюнктивную нормальную форму и сформировано множество дизъюнктов, на которые распадаются все подформулы. Два дизъюнкта этого множества, содержащие пропозициональные переменные с противоположными знаками (контрарные атомы) формируют третий дизъюнкт — резольвенту, в которой будут исключены контрарные пропозициональные переменные. Неоднократно применяя это правило к множеству дизъюнктов и резольвент, стремятся получить пустой дизъюнкт. Наличие пустого дизъюнкта свидетельствует о выполнении условия F1&F2&F3&…&Fn&ùB=л.

 

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