Синтез логических программ

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

Рассмотрим целенаправленный вывод процедур.

Предположения.

S – правильная непротиворечивая спецификация.

S – записана на языке логики 1 порядка.

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

Каждая процедура логически выводится из S.

Используется целенаправленный вывод.

В примере верификации (P, G) предложение D4 имеет вид:

D4: подмножество(X, Y) <=> B1 V B2.

Из него получены 2 процедуры

подмножество(X, Y):- B1.

подмножество(X, Y):- B2.

Предложения типа D4 могут иметь более сложную правую часть.

Целенаправленный вывод позволяет выводить каждую процедуру отдельно из S.

Суть целенаправленного вывода.

Целенаправленный вывод процедур для какого-либо отношения r начинается с целевого утверждения

G1:? r()

Вывод заканчивается целевым утверждением

Gn:? r1(), …, rn().

Поэтому r():- r1(), …, rn()

Поскольку

S, G1 |= G2

S, G2 |= G3 } S, G1 |= Gn в силу транзитивности отношения |=.

…

S, Gn-1 |= Gn

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

Последнее отношение можно записать в виде:

S, Ør() |= (r1(), …, rn()).

По теореме о дедукции получим:

S |= (r() ¬ r1(), …, rn()).

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

Пример. Найти все пары (U, V) элементов множества Z, удовлетворяющие бинарному отношению P(U, V).

Зависимость между U, V, Z можно записать предикатом найти(U, V, Z).

Спецификации имеют вид:

найти(U, V, Z) <=> U Î Z, V Î Z, P(U, V).

U Î Z <=> Z = W: Z’, (U = W V U Î Z’).

Выберем систему резолютивного вывода и преобразуем предложения 1 и 2 к предложениям вида:

S1: найти(U, V, Z) ¬ U Î Z, V Î Z, P(U, V).

S2: U Î Z ¬ найти(U, V, Z).

S3: V Î Z ¬ найти(U, V, Z).

S4: P(U, V) ¬ найти(U, V, Z).

S5: U Î U: Z’.

S6: U Î W: Z’ ¬ U Î Z’.

Отношение P(U, V) не специфицировано.

Начнем синтез программы поставив наиболее общее целевое утверждение.

G1:? найти(U, V, Z).

Из S1 и G1 получим G2:

G2:? U Î Z, V Î Z, P(U, V). по принципу резолюций

Выберем общую (стандартную) стратегию управления

G3:? V Î U: Z’, P(U, V). { Z:= U: Z’ }

G4:? P(U, U). { V:= U }

Вывод следует закончить на предложении G4, так как если его продолжать, включив предложение S4, то придем к правой части, содержащей предикат «найти».

Таким образом, получена процедура:

найти(U, V, Z) ¬ P(U, U). Θ = { Z:= U: Z’, V:= U }

Из S выведена процедура вида:

P1: найти(U, U, U: Z’) ¬ P(U, U).

P1 определяет предикат «найти» для частного случая, когда U и V – первый элемент множества Z.

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

Таким образом, с помощью back-tracking-а (возврата к ветвлению) можно получить все процедуры, описывающие знания о поставленной задаче из множества S1, …, S6.