Cтраница 2
Мы хотим определить, является ли С следствием S, используя технику поиска, основанную на m - абстракции. Таким способом процедура proofsearch 2 может быть приспособлена для проверки, является ли обычный дизъюнкт С логическим следствием множества обычных дизъюнктов S. Так как доказательства У существуют для всех D f ( C), если С - логическое следствие S, процедуры proofsearch 3 и proofsearch 4 также можно приспособить для выполнения указанной проверки. Заметим, что если найдено какое-либо m - резолюционное доказательство Т из S такого m - дизъюнкта С1, что Set ( Cl) поглощает С1, то из теоремы 3.4 нам известно, что некоторый обычный дизъюнкт С2, поглощающий Set ( Cl) ( а значит, и С), выводим из S обычной резолюцией. Поэтому С является логическим следствием из S тогда и только тогда, когда такое доказательство Т существует. [16]
Предположим, что мы ищем доказательство m - дизъюнкта С из S. Если существует доказательство Т m - дизъюнкта С из 5, имеющее глубину d, то существуют доказательства Т1 - ш-дизъюнктов В, из ft ( S) ( l / &), такие что T - ftTi и Tt является начальным поддоказательсгвом Vi. Более точно, W будет начальным поддоказательством доказательства, порожденного процедурой match. С этой целью необходимо модифицировать ndfindm так, чтобы она могла обращаться с векторными m - резолюционными доказательствами. В результате получается стратегия доказательства теорем proofsearch4, полностью аналогичная proofsearch 2, за исключением того лишь, что proofsearch 4 использует одновременно несколько абстракций. [17]