Общие принципы логических программ. Выполнение программ

Структура программы:

1. DOMAINS – вводятся новые типы переменных (область интерпретации);

Пример:

Name=char

Birthday=data (int,char,int)

2. PREDICATES – определение предикат;

Пример:

Person (name, phone)

3. СLAUSES – логические утверждения (факты, база данных);

Пример:

Person (Сидоров,2345678)

4. GOAL – цель – логическое утверждение.

Указанные цели опровергаются логическим выводом, включающим применение:

- резолюции;

- унификации;

- интерпретации.

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

Пример:

1.если a, то b

a®b

ùaÚb

На Прологе: b:-a b

- граф интерпретации

голова условие a

Факты: - А(а)a$xA(x) A(x)

A(a)

2. если а, то b&c b c

a®b&c

ùaÚb&c a

(aÚb)&(ùaÚc)

3.если c&b, то a a

ùcÚùbÚa граф «И»

Пролог: a:-c,b b c

4.если cÚb, то a

ùb&ùcÚa a

(ùbÚa)&(ùcÚa) граф «ИЛИ»

a:-b b c

a:-c

5. a®bÚc запрещено (не Хорновские)

ùaÚbÚc

6.отрицательный дизъюнкт

ùa ù(a&b) ù(aÚb)

:-a:-a,b:-a

:-b

Пример: применение Пролога для доказательства теорем в Хорновских дизъюнктах

a(x)p(x)&q(x,y) 1.a(x)Úùp(x) «И»

a(x)q(y,x)&r(y) 2.a(x)Úùq(x,y) «ИЛИ»

p(d) 3.a(x)Úùr(y) «И»

q(b,c) 4.a(x)Úùq(y,x)

r(d) 5.p(d)

r(b) 6.q(b,c)

a(z) 7.r(d) «ИЛИ»

8.r(b)

a(z)

a(x)

и_­1 или_­1 и_­2

p(x) q(x,y) r(y) q(y,x)

или_­2

p(d) q(b,c) r(d) r(b) q(b,c)

1. ùa(x) a(x)Úùp(x)

x=z - по правилу резолюций

ùp(x)

2.p(d)

z=d

продолжение по «И»

3. ùa(d) a(x)Úùq(x,y)

x=d

ùq(d,y)

4.q(b,c)

нет унификации

1. переход по «ИЛИ_­1»

ùa(z) a(x)Úùr(y)

x=z

ùr(y)

2.r(d)

y=d

переход по ИЛИ_­2

3.r(b) ùr(y)

y=b

переход по И_­2

4.ùa(z) a(x)Úùq(y,x)

x=z

ùq(y,z) – y=d

5. q(b,c) ùq(y,z)

нет унификации

переход по «ИЛИ_­2»

q(b,c) ùq(y,z)

y=d

z=c

Вывод закончен, так как пройдены все «И» и «ИЛИ» правила, получен пустой дизъюнкт. Формула общезначима.

Вывод по правилу резолюций упорядочен обходом «И» «ИЛИ» графов.Эта процедура называется Backtracing.