21195

Алгоритмы решения логических задач

Лекция

Информатика, кибернетика и программирование

Используя дедуктивную логику из двух или нескольких исходных аксиом имеющихся в логической базе знаний можно вывести очередное утверждениеследствие или доказать истинность ложность целевого утверждения теоремы путем использования определенных правил вывода. Этот процесс получения новых знаний из имеющихся аксиом называют логическим выводом на знаниях. Основными типами логических задач которые решаются с использованием метода резолюций являются следующие: а задача вывода следствий в которой нужно найти все утверждения которые можно...

Русский

2013-08-02

57 KB

32 чел.

PAGE  3

\\Лекция №8

8. Алгоритмы решения логических задач

8.1. Метод  резолюций\\

В основу современных методов решения логических задач положены формальные конструкции дедуктивной логики с использованием силлогизмов Аристотеля, основанных на логике утверждений (суждений). Например, из двух утверждений: "Все люди смертны" и "Аристотель – человек" следует вывод: "Аристотель смертен".

\\Используя дедуктивную логику, из двух или нескольких исходных аксиом, имеющихся в логической базе знаний, можно вывести очередное утверждение-следствие или доказать истинность (ложность) целевого утверждения (теоремы) путем использования определенных правил вывода. Этот процесс получения новых знаний из имеющихся аксиом называют логическим выводом на знаниях.

Основным методом решения логических задач на основе логического вывода является метод резолюций. Утверждение, выведенное из двух или нескольких аксиом с использованием метода резолюций, называется резольвентой. Этот метод был разработан Эрбраном в 1930г. и практически реализован Дж.Робинсоном в 1963г.

Основными типами логических задач, которые решаются с использованием метода резолюций, являются следующие:

а) задача вывода следствий, в которой нужно найти все утверждения, которые можно логическим путем вывести из исходных аксиом базы знаний, т.е. найти все следствия из заданных аксиом;

б) задача автоматического доказательства теорем, в которой необходимо установить, является ли теоремой данное утверждение, т.е. можно ли его вывести из аксиом базы знаний.

Доказательство теорем с использованием метода резолюций осуществляется в следующем порядке.

1) Теорема доказывается от противного, т.е. в базу знаний вводится отрицание того утверждения, которое требуется доказать. Например: если требуется доказать теорему  P (а), то в базу знаний вводят  утверждение  ~ P (а).

2) Если один и тот же предикат (литерал) находится в составе одной аксиомы (фразы Хорна) и с отрицанием - в другой аксиоме, то эти аксиомы являются резольвентными (резолирующими), а резольвента образуется в результате объединения обеих аксиом с исключением дублирующих предикатов. Например,  две аксиомы P (х) ~ Q (y, z)  и  Q (y, z) ~ R (y, z)  являются  резольвентными  и  резольвента  записывается как  P (х) ~ R (y, z).

3)  Переменная может быть заменена константой или другим термом.  Например, две аксиомы  P (х)  ~ Q (а, b)  и  Q (x, y)  ~ R (x, y)  являются  резольвентными.  При этом  переменная  x сопоставляется  с константой а,  переменная  y - с константой  b,  а  резольвента записывается как  P (a)   ~ R (a, b).  В ней  переменные заменены константами.

4) Аксиома-факт может резолировать с любым предикатом аксиомы-правила по схеме, указанной в п.2. Например, из факта  Q (a, b)  и правила  P (x, y) ~ Q (x, y)  образуется  резольвента-факт  P (a, b).

5) Разные  константы  не  сопоставляются  одна  с  другой,  поэтому  аксиомы  P (a)  ~ Q(a, b) и   Q (а, c)  ~ R (b, с)   не являются  резольвентными.

6) Если в процессе доказательства теоремы получились любые две противоречивые аксиомы типа  P (а)  и  ~ P (а),  то их резолюцией является пустая фраза (противоречие) , которое означает, что предположение о ложности (отрицании) исходной теоремы неверно. \\Следовательно, теорема является истинной и процесс доказательства на этом заканчивается.

Следует отметить, что все  резольвентные аксиомы остаются в составе базы знаний без изменений, а все резольвенты, полученные в процессе доказательства теоремы, добавляются в базу знаний, образуя новые знания о предметной области.


8.2. Пример использования метода резолюций

Рассмотрим пример использования метода резолюций для решения следующей задачи. Пусть база знаний о предметной области "Отцы и дети" состоит из фактов:

Боб является сыном Кости,

Костя является сыном Олега

и  правил:   если  x  является  сыном  y,  то x – потомок  y;

если  y  является  сыном  z,  то y – потомок  z;

если  x  является  потомком  y,   а  y – потомок  z,   то x – потомок  z.

Требуется доказать, что  Боб является потомком Олега.

В соотвествии с методом резолюций решение поставленной задачи может быть осуществлено следующим образом.

1) Введем константы:    B – Боб,   K – Костя,   O – Олег

и  предикаты:  S ( x, y )  -  x  является сыном  y;

P ( x, y )  -  x   является потомком  y.

2) Представим аксиомы (факты и правила) базы знаний в пренексной нормальной форме (7.2):

S ( B, K ); S ( K, O );

х у ( S ( x, y )    Р ( х, у ) );

х у ( S ( y, z )    Р ( y, z ) );

х у ( ( ( Р ( x, y )  & Р ( y, z ) )    Р ( х, z ) ).

Требуется доказать  истинность утверждения (теоремы):

Р ( B, O )      (8.1)

3) Исключая кванторы обобщения и учитывая преобразования табл.7.2, представим аксиомы базы знаний в виде фраз Хорна:

S ( B, K ) S ( K, O )

~ S ( x, y )    Р ( х, у )

~ S ( y, z )    Р ( y, z )

~ Р ( x, y )    ~ Р ( y, z )   Р ( х, z )

4) В соответствии с методом резолюций добавим к аксиомам базы знаний отрицание теоремы  (8.1):

~ Р ( B, O )       (8.2)

S ( B, K )       (8.3)

S ( K, O )       (8.4)

~ S ( x, y )    Р ( х, у )     (8.5)

~ S ( y, z )    Р ( y, z )      (8.6)

~ Р ( x, y )    ~ Р ( y, z )   Р ( х, z )    (8.7)

5) Применяя резолюцию к утверждениям (8.5) и (8.7), получим резольвенту:

~ S ( x, y )   ~ Р ( y, z )   Р ( х, z )    (8.8)

6) Сопоставляя в утверждениях (8.2) и (8.8)  переменные  x  с  B  и   z  с  O,  получим:

~ S (B, y )    ~ Р ( y, O )     (8.9)

7) Из (8.3) и (8.9) следует: ~ Р ( K, O )      (8.10)

8) Из (8.4) и (8.6) получим:    Р ( K, O )      (8.11)

9) Применяя резолюцию к утверждениям (8.10) и (8.11), получим пустую фразу.

Это означает, что теорема (8.1) является истинной.


8.3. Другие алгоритмы решения логических задач

Наряду с методом резолюций существуют другие алгоритмы решения логических задач, к числу которых относятся:

а) полный перебор возможных вариантов с целью нахождения оптимального решения;

б) эвристические методы исключения неперспективных вариантов с использованием эвристик – правил, не имеющих строгого математического обоснования;

в) планирование целесообразного поведения, когда общая цель решения задачи (запрос пользователя) развертывается в подцели, которые, в свою очередь, разбиваются на подзадачи  до тех пор, пока очередная подзадача не будет легко алгоритмизируемой.

Рассмотрим пример использования алгоритма полного перебора вариантов для решения задачи  экспертной системы (раздел 4.11)  по определению объекта, который:

а) имеет колеса;   б) не имеет винта;   в) не имеет крыльев;    г) возит грузы.

Эта задача в терминах предикатов, введенных в разделе 7.4, может быть сформулирована следующим образом: установить значение переменной x,  для которой истинно утверждение:

Q( x )  P( x, kls ) & ~ P( x, vnt ) & ~ P( x, krl ) & P( x, vgr ). (8.13)

Эту задачу можно решить методом прямого перебора утверждений базы знаний раздела 7.4, позволяющего установить, что истинное значение предиката Q(x), соответствующее истинному значению утверждения  (8.13), достигается для   x  grz.

Таким образом, искомым объектом является грузовик.

Алгоритм полного перебора вариантов является крайне неэффективным, поскольку для решения сложных (в частности – творческих) задач может потребоваться неприемлемо длительное время работы современной интеллектуальной системы.

8.4. Особенности логического вывода на знаниях

Логический вывод на знаниях с использованием метода резолюций может быть применен в небольшом числе случаев, когда предметная (проблемная) область, в которой решается задача, полностью известна и может быть формально описана в виде фактов и провил. Но большинство задач, где интеллект человека позволяет находить нужные решения, связано с областями, в которых знания человека (эксперта) принципиально неполны, неточны, некорректны. В этих условиях нет надежды из недостоверных знаний путем достоверного вывода получить что-либо абсолютно достоверное. Речь может идти только о правдоподобном выводе, при котором окончательный результат может быть получен лишь с некоторой оценкой уверенности в его истинности.

Кроме того, специалисты, работающие в плохо формализуемых областях (например, в медицине или психологии), рассуждают совсем не так, как представители точных наук. Для них весомым аргументом в пользу принятия определенного решения может служить мнение ряда признанных авторитетов в данной предметной области или сходство поставленной задач с известным доказанным аналогом.

Таким образом, использование логического вывода на знаниях возможно лишь в экстенсивной части знаний, когда четко перечислены все ситуации и для каждой из них определены классы возможных утверждений.

В промышленных системах искусственного интеллекта в той или иной мере используются различные модификации и расширения логических моделей с использованием индуктивных логик, логик «здравого смысла», логик веры, немонотонных рассуждений, нечетких логик и др., имеющих мало общего с классической математической логикой.


 

А также другие работы, которые могут Вас заинтересовать

61296. Волейбол 23.27 KB
  Ходьба в колонне по одному А на носках руки в стороны Б на пятках руки за головой В на внешней стороне стопы руки на поясе Г перекатами с пятки на носок Д в полуприседе руки на коленях Е в приседе руки на поясе...
61298. Нравственность и здоровье. Формирование правильного взаимоотношения полов 44.63 KB
  Руси качество относящееся к одной половине духовного быта другая половина ум умственное но составляющее общее с ней духовное начало: к умственному относится истина и ложь к нравственному добро и зло В. Типичные до свадьбы мечты о семейном счастье нередко сменяются после нее разочарованиями друг в друге в семейной жизни.