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

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

Rl{Ui, ...,иш),-, Rp{Ul, ,Um); (2.7)

где Rj{ui, ...,Um) - атомарные формулы логики первого порядка, буквы щ - термы.

Выполнение программы состоит в попытке решить задачу, т.е. доказать целевое утверждение (2.7), используя факты и предположения Л/i, ...,Мт,Wi,VVd, заданные в логической программе.

Описанные конструкции логического программирования семантически интерпретируются в логике предикатов. Процедура интерпретации состоит в сопоставлении формулам логической программы формул логики предикатов.

Для этого каждому факту (2.4) ставится в соответствие формула

y = yxi...yx,Pih,-,tn), (2.8)

где кванторы общности навешены на все переменные xi, ...,Ха атомарной формулы (2.4), входящие в термы tj (кроме переменных, в термах могут быть и константы).

Правилу (2.5) ставится в соответствие формула вида

g = \fyi...\fyr{Q,{8i,-,Sl)L...LQ,n{s,,...,8l)Q{8l,...,8l)), (2.9)

где кванторы общности, как и выше, навешены на все переменные, входящие в термы Si-

Запрос (2.7) получит в соответствие формулу

Hz = \/Zl...\/Zd{Ri{ui,...,Uru)L...LRp{ui,...,Uru)), (2.10)

где кванторы существования связывают все переменные.

Пусть Ji,...,Ja - формулы, соответствующие всем фактам, Gi,Gb - всем правилам. Тогда значение пары <программа, за-прос> есть утверждение о том, что формула Tiz есть логическое следствие формул .Fi,.Fa, 5i,5ь. Для того чтобы выяснить, так jm это, применяется метод резолюций.

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

Рассмотрим действия интерпретатора на примере следующей логической программы:

R{a,b). Q{b,g{c)).

Pix,fiy)):-Rix,z),Qiz,fiy)). (2.11)

P{x,f{y)):-R{x,z),Q{z,g{y)).

R{x,z):-Q{f{x),G[z)).

Здесь a, b,c,d- константы, x,y, z - переменные.

Предпсиюжим, что целевой запрос есть формула

P{u,f{v)). (2.12)

При вычислении ответа на этот запрос интерпретатор формулирует цель Р{и, f{v)) и пытается достичь ее, унифицируя цель с фактами. В нашем случае цель Р{и, f{v)) не унифицируется ни с одним из фактов. Тогда интерпретатор пытается ее унифицировать с заголовком одного из правил.

Это возможно с заголовком первого правила при подстановке < х\и >,< y\v >. Но надо предварительно проверить истинность предположений первого правила. Для этого интерпретатор формирует запрос

Rix,z),Qiz,fiy)).

Цель R{x, z) достигается за счет унификации с первым фактом с помощью подстановки <а;а>,<гЬ>.В таком случае, следую шдм запросом является Q{b, f{y)). Но эта цель не достижима, поскольку не унифицируется ни с одним из фактов.

Интерпретатор возвращается к цели R{x, z) и обращается к второму правилу.

Теперь интерпретатор делает запрос:

R{x,z),Q{z,g{y)).

Цель R{x,z) достигается, как мы знаем, унификацией с первым фактом при подстановке < х\а >,< z\b >, а цель Q{b, д{у)) достигается в силу того, что унифицируется со вторым фактом с помощью

подстановки < у\с >. Следовательно, цель (2.12) достигается подстановкой < и\а >,< v\c >. Поэтому интерпретатор на этом может закончить работу и выдать найденную подстановку. Выполнение программы считается успешно завершенным; при этом виден пример доказательства формулы (2.12).

2.6.2. Языки логического программирования

Для peajm3anHH идей логического программирования разработаны различные языки логического программирования. Первым и наиболее известным является язык PROLOG.

В TURBO PROLOG структура логической программы имеет следующий вид:

domains <структуры и типы даншлх>

global domains <внешние структуры и типы данных>

data base <глобальные предикаты динамической базы данных>

predicates <определение предикатов>

global predicates < внешние предикаты >

goal <цели>

clauses <факты и правила>

Пример 2.1. Логическая программа для выяснения родственных связей: domains name=Symbol predicates parent {паше,паше) father{name,name) mother{name,name) grandfather(name,name) grandmather(name,name)

clauses

шother(oля,пeтя).

father(THMyp,neTH).

father{тимyp,лeнa).

шother{ликa,киpилл).

шother(ликa,викa).

father(cepreй,киpилл).

mother(жeня,иpa).

father(тoля,фeдя).

father(тoля,иpa).

parent{X,Y):- mother{X,Y),father{X,Y). grandfather{X,Y):- father{X,Z),parent{Z,Y). grandmather(X,Y):- mother(X,Z),parent{Z,Y).