Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

Получили существенно более короткий список. Следовательно, стратегия вычеркивания может уменьшить потребную память для реализации метода резолюций. Ясно, что необходимые вычисления на начальном этапе увеличиваются. Чтобы использовать стратегию вычеркивания, нужно решать, является ли полученный дизъюнкт тавтологией или является ли один из дизъюнктов наддизъюнктом другого. Метод резолюций, как уже указано, позволяет автоматизировать доказательство теорем. Видно, что неограниченное применение резолюции может порождать много лишних и ненужных дизъюнктов наряду с полезными. Можно использовать стратегию вычеркивания, чтобы выбросить некоторые из ненужных и бесполезных дизъюнктов после того, как они порождены, но на их порождение уже потеряно время. Далее, если порождены ненужные дизъюнкты, то потребуются ресурсы машинного времени для того, чтобы определить, что эти дизъюнкты действительно лишние. Поэтому для получения эффективных процедур следует не допускать порождения большого числа бесполезных дизъюнктов. Имеются различные подходы к уменьшению вычислений, среди них: метод семантической резолюции, лок-резолюция, линейная резолюция и другие методы. Рассмотрим лок-резолюцию. § 5. Лок-резолюция Идея лок-резолюции состоит, в использовании индексов для упорядочения литер в дизъюнктах из данного множества S дизъюнктов. Иными словами, она включает введение индексов для каждого вхождения литеры в S некоторым целым числом; разные вхождения одной и той же литеры могут быть индексированы по-разному. После этого отрезать (удалять) разрешается только литеры с наименьшим индексом в каждом из дизъюнктов. Литеры в резольвентах наследуют свои индексы из посылок. Если литера в резольвенте может унаследовать более одного индекса, то ей ставится в соответствие наименьший индекс. Рассмотрим следуюш,ие два дизъюнкта: PvQ, -^vQ. Введем индексы, которые будем писать слева снизу от литеры: i^)lPV2Q, (2) 3 —PV4Q. Так как индекс 1 в jP меньше чем индекс 2 в 2Q, то разрешается отрезать ]Р. В 3 —Pv 4Q разрешается отрезать 3 —Р, так как 3<4. Таким образом, применяя правило резолюции к дизъюнктам (1) и (2) по jP и 3 —Р, получаем следуюш,ий дизъюнкт: i^)2QV4Q. 66