Съдържание 
 

ПРЕИМЕНУВАЩИ СУБСТИТУЦИИ.  ВАРИАНТИ НА ПОЛОЖИТЕЛНА ХОРНОВА КЛАУЗА

    Преименуваща субституция за дадено множество от променливи ще наричаме такава субституция, която съпоставя на променливите от това множество различни помежду си променливи, а на всяка друга променлива съпоставя самата нея. Ясно е, че тъждествената субституция е преименуваща за всяко множество от променливи, включително и за празното, за което тя е единствената преименуваща субституция, а ако ξ1, , ξm (m>0) са различни помежду си променливи, то преименуващи субституции за множеството 1,m} са точно субституциите от вида 11,mm], където η1, , ηm също са различни помежду си променливи (разбира се, такива субституции има безбройно много и тъждествената субституция е една от тях).

    Множество на променливите на дадена положителна хорнова клауза ще наричаме обединението на множеството на променливите на нейното заключение и множествата на променливите на атомарните формули, които са членове на нейната предпоставка. Очевидно това множество е винаги крайно (може евентуално да е празно    тогава клаузата се нарича затворена). Вариант на една хорнова клауза C ще наричаме всяка хорнова клауза от вида Cσ, където σ е преименуваща субституция за множеството на променливите на C (от твърдение 3 от въпроса Субституции е ясно, че в такъв случай множеството на променливите на Cσ ще се състои от променливите ξσ, където ξ принадлежи на множеството на променливите на C). Очевидно всяка клауза е вариант на себе си и ако клаузата е затворена, тя е единственият свой вариант, докато в останалите случаи вариантите й са безбройно много.

    Твърдение 1. Нека C е положителна хорнова клауза. За всяко крайно множество Ξ° от променливи може да се намери вариант на C, на който множеството на променливите няма общи елементи с Ξ°.

    Доказателство. Нека Ξ° е произволно крайно множество от променливи. Благодарение на това, че множеството на всички променливи е безкрайно, съществува субституция, която е преименуваща за множеството на променливите на C и на всяка променлива от това множество съпоставя променлива, непринадлежаща на Ξ°. Прилагайки такава субституция към клаузата C, получаваме неин вариант с желаното свойство. 

    Твърдение 2. Нека C е положителна хорнова клауза, а C е вариант на C. Тогава C е вариант на C.

    Доказателство. Нека σ е такава субституция, преименуваща за множеството на променливите на C, че да имаме равенството C = Cσ. Очевидно съществува субституция σ, която е преименуваща за множеството на променливите на клаузата C и е такава, че (ξσ)σ = ξ за всяка променлива ξ от множеството на променливите на C. Ще покажем, че C = Cσ. Тъй като

Cσ = (Cσ)σ = C(σσ),
достатъчно е да покажем, че върху множеството на променливите на клаузата C субституцията σσ съвпада с тъждествената. Това обаче е ясно от избора на субституцията σ и от равенството (ξσ)σ = ξ(σσ). 

    Следствие. Нека Q и R са хорнови запитвания, σ е субституция, C е положителна хорнова клауза, а C е вариант на C. При тези предположения може да се твърди, че R е резолвента на Q и C посредством σ точно тогава, когато R е резолвента на Q и C посредством σ.

    Доказателство. При направените предположения всяка от клаузите C и C е частен случай на другата, следователно частните случаи на тези две клаузи са едни и същи. От друга страна в дефиницията за резолвента на хорново запитване и положителна хорнова клауза клаузата играе роля само чрез частните си случаи. 

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