Математическая логика и теория алгоритмов

ния, чтобы выбросить некоторые из этих ненужных и бесполезных дизъюнктов после того, как они порождены, на их порождение уже потеряно время. Далее, если порождены бесполезные дизъюнкты, то нужны большие ресурсы машинного времени для того, чтобы опреде­ лить, что эти дизъюнкты действительно лишние и ненужные. Поэтому для получения эффективных процедур следует не допз'скать порояаде- ния большого. числа бесполезных дизъюнктов. Имеются различные подходы к уменьшению вычислений, среди них; метод семантической резолюции, лок-резолюция, линейная резолюция и другие методы. Рассмотрим лок-резолюцию. Хорошее вдвойне хорошо, если коротко. Бальтасар Грасиан § 6. Лок-резолюция Идея лок-резолюций состоит, по существу, в использовании ин­ дексов для упорядочения литер в дизъюнктах из данного множества s дизъюнктов. Иными словами, она включает введение индексов для каждого вхождения литеры в s некоторым целым числом; разные вхождения одной и той же литеры могут быть индексированы по-разному. После этого отрезать (удалять) разрешается только лите­ ры с наименьшим индексом в каждом из дизъюнктов. Литеры в резольвентах наследуют свои индексы из посылок. Если литера в резольвенте может унаследовать более одного индекса, то ей ставит­ ся в соответствие наименьший индекс. Рассмотрим следующие два дизъгонкта: pvq, 1 Pv0, Введем индексы, которые будем писать слева сшзу от литеры; (1) vPvjQ, (2) alPv^Q. Так как индекс 1 в ]Р меньше чем индекс 2 в гй, то разрешается отрезать В з1 PV4Q разрешается отрезать 3IР, так как 3<4. 98