Метод модификации посылок

Абдуктивный метод модификации посылок позволяет удовлетворить требованиям выводимости для множества заключений. Метод основан на трех методах нижнего уровня: методе определения выводимости, методе добавления посылок и методе удаления посылок. Метод определения выводимости позволяет установить, выводится ли заданное заключение из набора исходных посылок, и является методом дедуктивного логического вывода. Метод добавления посылок [Котельников, 2005] позволяет для заданного заключения генерировать семейство множеств дополнительных посылок. При добавлении любого множества из найденного семейства заключение становится логическим следствием исходных посылок.

При помощи метода удаления посылок [Котельников, 2006] осуществляется поиск удаляемых посылок среди множества исходных посылок для заданного заключения. Результатом метода является семейство множеств посылок-кандидатов на удаление.

В абдуктивном методе модификации посылок можно выделить пять шагов. Введем обозначение: h — счетчик числа итераций, h=1.

На первом шаге модификации посылок все заключения, принадлежащие множеству m, с помощью метода определения выводимости делятся на четыре класса:

p/p — логический вывод успешен / должен быть успешен. Заключения этого класса обозначим d^pp_k (k=1.K);

n/p — логический вывод неудачен / должен быть успешен. Обозначим такие заключения d^np_l (l=1.L);

p/n — логический вывод успешен / должен быть неудачен. Заключения обозначим d^pn_r (r=1.R);

n/n — логический вывод неудачен / должен быть неудачен. Заключения обозначим dⁿⁿ_s (s=1.S).

Проверяется, имеются ли заключения в классах p/n и n/p. Если заключения в обоих классах отсутствуют, то происходит переход к шагу 5. Иначе выполняется следующий шаг.

На втором шаге находятся множества посылок, соответствующие классам n/p и p/n:

для каждого заключения d^np_l класса n/p генерируется семейство множеств посылок ^np_l. Семейство множеств ^np_l состоит из множеств M^np_li (i=1.I). При добавлении любого множества M^np_li заключение d^np_l становится выводимым. Генерация осуществляется методом добавления посылок;

метод удаления посылок применяется для нахождения семейства множеств ^pn_r для каждого заключения d^pn_r класса p/n. Семейство множеств ^pn_r состоит из множеств M^pn_rj (j=1.J). При удалении любого множества M^pn_rj из множества исходных посылок вывод заключения d^pn_r заканчивается неудачно.

На третьем шаге с помощью проверочного дедуктивного вывода определяются множества посылок из семейств множеств ^np_l, которые можно включить во множество исходных посылок без влияния на отсутствие выводимости заключений класса n/n. Если такие множества найдены, то они добавляются во множество М исходных посылок, а соответствующие заключения из класса n/p переходят в класс p/p. Остальные заключения остаются в классе n/p до следующего цикла или до окончания решения, так как на текущем шаге добавление посылок из множества M_np вступает в противоречие с требованием отсутствия выводимости заключений класса n/n.

На четвертом шаге находятся такие множества посылок семейств ^pn, которые можно удалить без влияния на выводимость заключений класса p/p. Найденные множества удаляются из множества М исходных посылок, а соответствующие заключения d^pn_r из класса p/n переходят в класс n/n. Остальные дизъюнкты остаются в классе p/n до следующего цикла или до окончания решения, так как на текущем шаге удаление соответствующих посылок вступает в противоречие с требованием выводимости заключений класса p/p.

На пятом шаге проверяется, имеются ли заключения в классах p/n и n/p и меньше ли счетчик заданного максимального значения: hmax. Если заключения в обоих классах отсутствуют, то модификация посылок заканчивается и фиксируется положительный результат — модифицированное множество исходных посылок М. Если счетчик превысил максимальное значение и имеются заключения хотя бы в одном классе p/n или n/p, то модификация посылок заканчивается и фиксируется отрицательный результат — за отведенное число шагов метод не смог привести множество исходных посылок в соответствие с требованиями выводимости.

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

Способом разрешения такой ситуации может служить безусловная модификация, когда некоторое множество M^np_li (M^pn_rj) безусловно добавляется (удаляется) во множество исходных посылок М. При прочих равных условиях предпочтение отдается множествам M^np_li. Причем среди множеств выбираются те, которые (как было выяснено на шагах 3 и 4) оказывают минимальное влияние на классы заключений p/p и n/n.

Определим, что понимается под минимальным влиянием. Из набора множеств M^np_li минимальное влияние на класс заключений n/n оказывает такое множество, при добавлении которого во множество исходных посылок М минимальное число заключений класса n/n переходит в класс p/n. Аналогично, из набора множеств M^pn_rj минимальное влияние на класс заключений р/р оказывает такое множество, при удалении которого из множества исходных посылок М минимальное число заключений класса р/р переходит в класс n/p.

Если сразу несколько множеств оказывают одинаковое минимальное влияние на классы заключений p/p и n/n, то предпочтение отдается множествам M^np_li. Если несколько множеств удовлетворяют одновременно всем перечисленным признакам, выбор осуществляется случайно. Если в классах p/n и n/p имеются заключения, то счетчик числа итераций h увеличивается на единицу, и если имеет место ситуация зацикливания, то осуществляется переход к шагу 1, иначе — переход к шагу 2.