9. Полнота резолютивного вывода. Стратегии резолютивного вывода. Вычислительные возможности метода резолюций (Лекции), страница 2

Проверка общезначимости формулДано: формула ϕ?Узнать: |= ϕРешение:I перейти к отрицанию формулыI построить равносильную ПНФI построить равновыполнимую ССФI перейти к системе дизъюнктовI резолютивно вывести Вычислительные возможностиметода резолюцийДля решения каких задач пригоден метод резолюций?II. Проверка логического следованияДано:I база знаний: набор формул ϕ1 , .

. . , ϕkI запрос: формула ϕУзнать: следует ли запрос из базы знанийРешение:{ϕ1 , . . . , ϕk } |= ϕ⇔|= ϕ1 & . . . & ϕk → ϕПроверка логического следованияобщезначимости формулысведенакпроверкеВычислительные возможностиметода резолюцийДля решения каких задач пригоден метод резолюций?III. Проверка наличия логически следующих примеровДано:I база знаний: набор дизъюнктов ϕ1 , . . . , ϕkI запрос: атом A(exn )Узнать: верно ли, что хотя бы один основной пример запросалогически следует из базы знанийРешение:I выписываем систему дизъюнктовS = {ϕ1 , . .

. , ϕk , ¬A(exn )}I проверяем выводимость из SВычислительные возможностиметода резолюцийДля решения каких задач пригоден метод резолюций?IV. Вычисление логически следующих примеровДано:I база знаний: набор дизъюнктов ϕ1 , . . . , ϕkI запрос: атом A(exn )Узнать: какие основные примеры запроса логически следуют избазы знанийВычислительные возможностиметода резолюцийДля решения каких задач пригоден метод резолюций?IV.

Вычисление логически следующих примеровРешение:I выписываем систему дизъюнктовS = {ϕ1 , . . . , ϕk , ¬A(exn )}I резолютивно выводим из SI выписываем унификаторы θ1 , . . . , θm , полученные припостроении выводаI последовательно применяем их к переменным запроса — иполучаем ответ:t1 = x1 θ1 . . . θm , . . . , tn = xn θ1 . .

. θmА в каких случаях и как именно это работает?Вычислительные возможностиметода резолюцийВот подходящий пример:IIIДаша любит Сашуϕ1 : L(Даша, Саша)ϕ2 : L(Саша, пиво)Саша любит пивоПаша любит пиво и всех тех, кто любит то же, что и онϕ3 : L(Паша, пиво)ϕ4 : ∀x ∀y (¬L(Паша, y) ∨ ¬L(x, y) ∨ L(Паша, x))Кто любит Дашу?ϕ0 : L(z, Даша)Система дизъюнктов:S = {¬ϕ0 , ϕ1 , ϕ2 , ϕ3 , ϕ4 }Попробуем построить вывод из SВычислительные возможностиметода резолюций¬L(z, Даша)¬L(Паша, y1 ) ∨ ¬L(x1 , y1 ) ∨ L(Паша, x1 )θ1 = {z/Паша, .

. .}¬L(Паша, y) ∨ ¬L(Даша, y)L(Даша, Саша)θ2¬L(Паша, Саша)¬L(Паша, y2 ) ∨ ¬L(x2 , y2 ) ∨ L(Паша, x2 )θ3¬L(Паша, y) ∨ ¬L(Саша, y)L(Саша, пиво)θ4¬L(Паша, пиво)L(Паша, пиво)θ5Вычислительные возможностиметода резолюцийКакие же ответы мы можем из этого получить?Система дизъюнктов S противоречиваЗначит, кто-то любит ДашуНо кто же это?Вернёмся к запросу:L(z, Даша)Попробуем применить унификаторы θ1 , . . . , θ5 к переменной z:z {z/Паша, .

. .} θ2 θ3 θ4 θ5 = ПашаОтвет готов!Паша любит ДашуВопросы для самостоятельного размышления:Кто любит пиво?Кого любит пиво?Вычислительные возможностиметода резолюцийА для любых ли систем дизъюнктов можно подобным образомнайти ответ?Оказывается,нетНапример, рассмотрим такую задачу:Если вечером будет дождь,то мы пойдём в кино,а если дождя не будет, то в паркГде мы проведём вечер?Вычислительные возможностиметода резолюцийГде мы проведём вечер?Запишем задачу на языке логики предикатовIIIконстанты: кино, паркR = “вечером будет дождь”E(x) = “вечером мы пойдём в x”База знаний: {R → E(кино), ¬R → E(парк)}Запрос: E(x)Получаем такую систему дизъюнктов:S = {¬R ∨ E(кино), R ∨ E(парк), ¬E(x)}Попробуем построить резолютивный вывод из SВычислительные возможностиметода резолюцийГде мы проведём вечер?¬R ∨ E(кино){x/кино}¬E(x)¬R{x/парк} R ∨ E(парк)Rуспех?Результат: {R → E(кино), ¬R → E(парк)} |= ∃x E(x)Но куда же мы пойдём?Всё, что мы можем сказать, — это: x ∈ {кино, парк}Мы смогли доказать, что пойдём куда-нибудь вечером,но не вычислили, куда именноВычислительные возможностиметода резолюцийЧтобы резолютивный вывод мог служить средствомвычисления, он должен быть конструктивнымЕстественный способ гарантировать наличие конструктивноговывода — ограничить круг решаемых задач и методы ихрешенияКонструктивным является, например, входной резолютивныйвывод, инициированный запросом задачи, если запросиспользуется только в начале выводаИменно такой вывод был получен в задаче “о пиве”А почему в задаче “о планах на вечер” не вышло построитьконструктивный вывод?Вычислительные возможностиметода резолюцийДизъюнкты базы знаний в задаче “о пиве” могут быть записаныв виде позитивной импликации[если <атом> и <атом> и .

. . и <атом>, то] <атом>:L(Даша, Саша)L(Саша, пиво)L(Паша, пиво)L(Паша, y) & L(x, y) → L(Паша, x)В базе знаний задачи “о планах на вечер” оказался дизъюнкт,состоящий из двух положительных литер:R ∨ E(парк)Такой дизъюнкт нельзя записать в виде позитивной импликацииВычислительные возможностиметода резолюцийХорновский дизъюнкт — это дизъюнкт, содержащий не болееодной положительной литерыПравило — это хорновский дизъюнкт, содержащий ровно однулитеруЗапрос — это хорновский дизъюнкт, не содержащий ни однойлитерыИ чем же хороши хорновские дизъюнкты?Вычислительные возможностиметода резолюцийУтверждение.

¬A1 ∨ · · · ∨ ¬Ak ∨ BУтверждение. ¬B1 ∨ · · · ∨ ¬Bk≈≈A1 & . . . & Ak → B¬(B1 & . . . & Bk )Правило — это описание того,I из каких фактов A1 , . . . , Ak мы можем необходимо получитьфакт B,I как решение задачи B сводится к решению задач A1 , . . . , Ak ,I ...Запрос — этоI набор фактов B1 , .

. . , Bk , которые мы хотим получить,I набор задач, которые хотим решить, обёрнутый отрицаниемдля проведения резолютивного вывода,I ...Вычислительные возможностиметода резолюцийУтверждение. Не более одной литеры правила можетобразовывать контрарную пару с литерой запросаУтверждение. Ни к какой паре запросов нельзяприменить правило резолюцииУтверждение. Резольвента запроса и правила являетсязапросомТаким образом,I входной вывод, инициированный запросом, для системыхорновских дизъюнктов, — это последовательное получениезапросов, основанное на применении к ним правил базызнанийI перебор всевозможных контрарных пар при полученииследующей резольвенты — это перебор литер последнегополученного запросаВычислительные возможностиметода резолюцийСтруктура хорновских дизъюнктов (а также некоторые ихсвойства, не затрагиваемые в курсе) идеально подходит дляэффективного построения входного вывода, инициированногозапросомВходной вывод конструктивен систем хорновских дизъюнктов,то есть пригоден для решения задачи вычисления логическиследующих из базы знаний примеров запросаПри этом хорновские дизъюнкты в сочетании с входнымвыводом оказываются настолько выразительными, а построениевходного вывода — настолько эффективным, что часто именнотакие дизъюнкты и такой вывод используются для решениявычислительных логических задач — например, в логическомпрограммировании, средствах автоматического доказательстватеорем, логических средствах работы с базами данных, .

. .Конец лекции 9.