Логическо програмиране 2004/05 - упражнения

Задача 1. "Всеки който може да чете е грамотен. Маймуните не са грамотни, но някои от тях са интелигентни. Докажете, че някой който е интелигентен не може да чете." Формулирайте задачата във формули и я докажете с метода на общата резолюция.

Задача 2. С метода на общата резолюция, докажете, че от формулите F₁, F₂ (и евентуално F₃) логически следва формулата G:

1. F₁: $$\forall Y(\exists X(p(X,Y))\rightarrow \neg s(Y,Y))$$
   F₂: $$\forall X\exists Y(s(Y,Y)\& \forall Z(q(Y,Z))$$
   F₃: $$\forall X\exists Y(r(X,X)\& q(X,Y)\rightarrow p(Y,X))$$
   

   ---

   G: $$\exists X\exists Y(\neg(s(X,Y)\rightarrow r(X,Y)))$$
   
   
2. F₁: $$\forall X\forall Y\exists Z((q(Z)\rightarrow p(X,Y)) \& \forall N(p(N,Z)\rightarrow r(X,N)))$$
   F₂: $$\forall X\exists Y(\neg p(X,Y) \& \forall Z(\neg p(Y,Z)\rightarrow q(Z)))$$
   

   ---

   G: $$\exists X r(X,X)$$
   
   
3. F₁: $$\forall X\exists Y\forall Z((q(Y)\rightarrow p(X,a)) \& p(Z,a)\rightarrow r(X,Z)))$$
   F₂: $$\forall X\forall Y\forall Z(\neg p(Y,X) \& (\neg p(Y,Z)\rightarrow q(Z)))$$
   

   ---

   G: $$\exists X r(X,X)$$
   
   
4. F₁: $$\exists X(p(X,f(X)) \& \neg p(f(X),X))$$
   F₂: $$\forall X\forall Y(p(X,Y)\rightarrow p(f(X),Y))$$
   

   ---

   G: $$\exists X\exists Y((p(f(X),X)\vee q(f(X),Y))\rightarrow p(X,X) \& q(X,X)))$$
   
   
5. F₁: $$\neg\exists X(p(X,X)\& q(X,X))$$
   F₂: $$\forall X\forall Y((q(X,Y)\rightarrow q(g(X),Y))\& (p(g(X),Y) \vee q(g(X),X)))$$
   

   ---

   G: $$\forall X(\neg q(X,g(X))\vee q(g(X),X))$$
   
   
6. F₁: $$\forall X\forall Y(p(X,Y)\rightarrow\neg s(Y,Y))$$
   F₂: $$\exists Y\forall Z(s(Y,Y)\& q(Y,Z)$$
   F₃: $$\forall X\exists Y(r(X,X)\& q(X,Y)\rightarrow p(Y,X))$$
   

   ---

   G: $$\exists X\exists Y(\neg(s(X,X)\rightarrow r(X,Y)))$$