Метод резолюции состоит в том, что имеется процедура постепенного подъема вверх по семантическому дереву, в результате которой неблагоприятные вершины поднимаются вверх по ярусам дерева. Подъем происходит до тех пор, пока это возможно. Если таким путем удастся дойти до корневой вершины, т. е. сделать все исходное семантическое дерево замкнутым, то тем самым будет доказана невыводимость F. [c.231]
Метод резолюции состоит в том, что имеется процедура постепенного подъема вверх по семантическому дереву, в результате которой неблагоприятные вершины поднимаются вверх по ярусам дерева. Подъем происходит до тех пор, пока это возможно. Если таким путем удастся дойти до корневой вершины, т. е. сделать все исходное семантическое дерево замкнутым, то тем самым будет доказана невыводимость F. [c.231]