Преименуваща субституция за дадено множество от променливи ще наричаме такава субституция, която съпоставя на променливите от това множество различни помежду си променливи, а на всяка друга променлива съпоставя самата нея. Ясно е, че тъждествената субституция е преименуваща за всяко множество от променливи, включително и за празното, за което тя е единствената преименуваща субституция, а ако ξ₁, …, ξ_m (m>0) са различни помежду си променливи, то преименуващи субституции за множеството {ξ₁,…,ξ_m} са точно субституциите от вида [ξ₁/η₁,…,ξ_m/η_m], където η₁, …, η_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′σ′. Тъй като

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

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

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