Лекция 5. Полнота табличного вывода. Теорема Левенгейма-Сколема... (1161876), страница 3
Текст из файла (страница 3)
Это касается правил (L∀) и (R∃).L∀hΓ, ∀xϕ(x)|∆ihΓ, ∀xϕ(x), ϕ(x){x/t}|∆iR∃hΓ|∆, ∃xϕ(x)ihΓ|∆, ∃xϕ(x), ϕ(x){x/t}iпоскольку выбор терма t правилами не оговаривается. Простойперебор всех термов практически невозможен. (почему ? )АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВОТЕОРЕМПотому что термов очень-очень много. Если есть одиндвухместный функциональный символ f (2) и две константыc1 , c2 , то с их помощью можно построить более 101000 основныхтермов высоты 10. Это количество значительно превосходитчисло наносекунд, прошедших с момента Большого Взрыва.Значит, нужно придумать способ, позволяющий быстро и точновычислять тот терм, который нужно подставлять вместопеременных, связанных кванторами.Эту задачу в 1964 г. сумели решить Дж.
Робинсон (методрезолюций) и С. Маслов (обратный метод ε-термов).КОНЕЦ ЛЕКЦИИ 5..
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
