3) Составляющая : Логические формулы

Правила построения формул:

а)константа сорта А, есть терм сорта А

б)переменная принимающая значение из сорта А, есть терм сорта А

в)если сигнатура содержит функцию-

построенные термы сортов соответственно, то

-есть терм сорта В

г)если сигнатура содержит предикат-

,термы построенных сортов

, то - есть атом.

д)если - термы одинакового сорта, то выражение , то есть атом

е)Атом есть формула правильно построенная (ППФ)Переменная, входящая в атом, является свободной в этом атоме.

ж)если построенная формула в которую свободно входит переменные х сорта А , то выражения:

также является ППФ, переменная “x” является

связанной (в новых файлах)

з)если уже построенные формулы, то , также

является ППФ

Примеры:

1) Представление Знания b=> опер2 выполнены на токарном станке

тип_ст(ст(опер2))=nток

2) Опер2 выполн на ост.1 на ст.1 нач 5 конец 12

)

3)

Лекция 8 12.11.99.

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

Метод резолюций доказывает невыполнимость.

Для использования этого метода необходимо исходную формулу привести к ДНФ.

ДНФ:

- дизъюнкция литер

рii – атом или отрицание атома.

Потом ДНФ представляют в виде множества дизъюнктов

В методе резолюций – имеется одно правило вывода

В результате из 2-х дизъюнктов получаем новую, называется руовентой

- получаем пустой дизъюнкт , который всегда ложный.

Если множество содержит пустой дизъюнкт , то оно является не выполнимым.

Получается пустой дизъюнкт, который доказывает что данное множество является невыполнимым.

Метод резолюций применяется до тех пор пока не получится пустой– дизъюнкт

m,n – const

подстановка вместо переменной константы –унификация.

В данном случае выполняем подстановку {n/y}:

Из (1)и (2) => a(x)c(x,n) (5)

Из (3) и (5) , выполняя ь подстановку {m/n}=> c(m,n) (6)

Из (4) и (6) без подстановок => 0

Принцип резолюций в Прологе

В Прологе используются хордовские дизъюнкты, т.е. дизъюнкты, содержащие одну литеру без отрицания.

На пример

=>

конъюнкция

без

отрицания

Могут использоваться дизъюнкты , которые вообще не содержат литер. –

это целевое утверждение на прологе: ? – a

a: - b,c,d.

b: - e,f.

c.

e.

f.

?-a

a(1)

a(2)

a(3)

Представление программы в виде графа

a: - b;c

b: - d,e

c: - g,f.

e: - i,h

g: - h,j

d.

f.

h.