Пример 1. Програмата от пример 1 от въпроса "Минимални ербранови модели" се представя от множеството, състоящо се от следните дизюнкти:

    Основните семантични свойства на представянето на хорновите цели и на хорновите клаузи чрез дизюнкти, както и на програмите чрез множества от дизюнкти, се изказват посредством следните твърдения:
        а) една хорнова цел G не е изпълнена в дадена структура S при дадена оценка v на променливите точно тогава, когато S,vdis(G);
        б) една хорнова клауза C е тъждествено вярна в дадена структура S точно тогава, когато дизюнктът dis(C) е тъждествено верен в S;
        в) една структура е модел за дадена хорнова програма P точно тогава, когато в нея са тъждествено верни всички дизюнкти от множеството setofdis(P).

    Първото от горните твърдения може да се докаже като се забележи, че G не е изпълнена в S при оценката v точно тогава, когато някой член на G не е верен в S при оценката v, а това означава някой литерал от дизюнкта dis(G) да е е верен в S при оценката v. Второто от твърденията се проверява така: при тяло B и глава H на C тъждествената вярност на C в S е равносилна с това при всяка оценка v в S на променливите, за която в S е изпълнена целта B, да имаме още и S,vH; това условие от своя страна е равносилно с условието за всяка оценка v в S на променливите целта B да не е изпълнена в S или да имаме S,vH, обаче (по първото от твърденията) целта B да не е изпълнена в S е равносилно с S,vdis(G) и остава само да се възпозваме от дефиницията на dis(C). Третото от твърденията следва непосредствено от второто.

    Сега сме готови да формулираме и докажем споменатата преди малко връзка между изпълнимост на хорнова цел при хорнова програма и неизпълнимост на подходящо множество от дизюнкти.

    Теорема за свеждане на задачите на логическото програмиране за изпълнимост към задачи за неизпълнимост на множества от дизюнкти. Нека P е произволна хорнова програма, а G е произволна хорнова цел.  Нека M=setofdis(P)Иdis(G). В такъв случай целта G е изпълнима при P точно тогава, когато множеството M е неизпълнимо.

    Доказателство. Целта G е изпълнима при P точно тогава, когато G е изпълнима във всеки модел за P, т.е. когато не съществува такава структура S, че S е модел за P, но G не е изпълнена в S при никоя оценка на променливите. Като се възползваме от току-що доказаните твърдения в) и а), виждаме обаче, че за да бъде една структура S модел за P, но G да не е изпълнена в S при никоя оценка на променливите, необходимо и достатъчно е в S да са тъждествено верни всички дизюнкти от множеството M. Следователно структура S със споменатите свойства ще съществува точно тогава, когато M е изпълнимо, и значи няма да съществува точно тогава, когато M е неизпълнимо.  _ї

    В множеството M, за което става дума в горната теорема, има точно един отрицателен дизюнкт - това е дизюнктът dis(G). Въпросът за изпълнимостта на това множество би могъл да се изследва по метода на резолюцията. Във връзка с това отбелязваме, че резолвента на отрицателен и на положителен хорнов дизюнкт е винаги отрицателен хорнов дизюнкт. Значи ако dis(G) има резолвента с някой дизюнкт от setofdis(P), тя пак ще бъде отрицателен хорнов дизюнкт. Ако и той има резолвента с някой дизюнкт от setofdis(P), и тази резолвента ще бъде отрицателен хорнов дизюнкт и т.н. Може да се докаже, че ако множеството M е неизпълнимо, този процес на последователно получаване на отрицателни хорнови дизюнкти може да се осъществи така, че да завърши с получаване на празния дизюнкт. Такъв начин на установяване на неизпълнимостта на множеството M е в духа на работата на Пролог при евентуалното установяване на изпълнимостта на G при P (възможно е обаче G да е изпълнима при P, а Пролог да не е в състояние да установи това).

    Пример 2. Целта, спомената в пример 1, е изпълнима при споменатата там програма, и един неин изпълним затворен частен случай е онзи, който се получава чрез субституцията [c5=:U] (това заключение може да се направи например като се покаже, че членовете на този частен случай са затворено изводими от програмата, а и използването на Пролог води до същото заключение). Ако искаме да използваме горната теорема, за да установим изпълнимостта на разглежданата цел при разглежданата програма, ще трябва да покажем, че е неизпълнимо множеството, състоящо се от дизюнктите

Последно изменение: 21.06.2000 г.
 

Previous  Next  Contents