Ovo su resenja zadataka iz metode rezolucije koja su kucana za vreme casa.
Da bi specijalni karakteri bili pravilno prikazani odabrati Unicode za character encoding


----------------------------------------------------------------------------------------------------------------------------------------------
3. zadatak -- nemimoilazne prave

R1  -- recenica 1

(R1 ∧ R2 ∧ R3) ⇒ R4 pokazujemo da je valjana
znaci metodom rezolucije pokazujemo da je negacija gornje formule kontradiktorna

¬[(R1 ∧ R2 ∧ R3) ⇒ R4]
¬[¬(R1 ∧ R2 ∧ R3) ∨ R4]
R1 ∧ R2 ∧ R3 ∧ ¬R4

(∀x)(∀y )(m(x, y ) ⇒ (s(x, y ) ∨ p(x, y )) ∧
(∀x)(∀y )(s(x, y ) ⇒ r (x, y )) ∧
(∀x)(∀y )(p(x, y ) ⇒ r (x, y )) ∧
¬(∀x)(∀y )(m(x, y ) ⇒ r (x, y ))


(∀x)(∀y )(¬m(x, y ) ∨ (s(x, y ) ∨ p(x, y )) ∧
(∀x)(∀y )(¬s(x, y ) ∨ r (x, y )) ∧
(∀x)(∀y )(¬p(x, y ) ∨ r (x, y )) ∧
¬(∀x)(∀y )(¬m(x, y ) ∨ r (x, y ))



(∀x)(∀y )(¬m(x, y ) ∨ (s(x, y ) ∨ p(x, y )) ∧
(∀x)(∀y )(¬s(x, y ) ∨ r (x, y )) ∧
(∀x)(∀y )(¬p(x, y ) ∨ r (x, y )) ∧
(∃x)(∃y )(m(x, y ) ∧ ¬r (x, y ))


(∃x)(∃y )(∀x1)(∀y1 )(∀x2)(∀y2 )(∀x3)(∀y3 )[
(¬m(x1, y1 ) ∨ s(x1, y1 ) ∨ p(x1, y1 )) ∧
(¬s(x2, y2 ) ∨ r (x2, y2 )) ∧
(¬p(x3, y3 ) ∨ r (x3, y3 )) ∧
  m(x, y ) ∧ 
  ¬r (x, y ) ]

  x--> c1   y --> c2 uvodimo nove konstante



(∀x1)(∀y1 )(∀x2)(∀y2 )(∀x3)(∀y3 )[
(¬m(x1, y1 ) ∨ s(x1, y1 ) ∨ p(x1, y1 )) ∧
(¬s(x2, y2 ) ∨ r (x2, y2 )) ∧
(¬p(x3, y3 ) ∨ r (x3, y3 )) ∧
  m(c1, c2 ) ∧ 
  ¬r (c1, c2 ) ]


1. ¬m(x1, y1 )   s(x1, y1 )   p(x1, y1 )
2. ¬s(x2, y2 )   r (x2, y2 )
3. ¬p(x3, y3 )   r (x3, y3 )
4. m(c1, c2 )
5. ¬r (c1, c2 )

6. (2, 5)  x2->c1   y2-->c2 
    ¬s(c1, c2 )

7. (3, 5)  x3--> c1   y3 ---> c2
    ¬p(c1, c2 )


8. (6, 1) x1--> c1  y1-->c2
   ¬m(c1, c2 )    p(c1, c2 )

9. (7, 8)
   ¬m(c1, c2 )

10, (9, 4)
    prazna klauza



-----------------------------------------------------------------------
8. zadatak  -- Janko i avion

R1 ∧ R2 ∧ R3 ∧ R4 -- metodom rezolucije pokazujemo da je kontradiktorna

(∀x)(va(x) ⇒ dz(x))  ∧
(∀x)(dz(x) ⇒ pr (x)) ∧
va(j)  ∧
¬pr (j)


(∀x)(¬va(x) ∨ dz(x))  ∧
(∀x)(¬dz(x) ∨ pr (x)) ∧
va(j)  ∧
¬pr (j)


(∀x)(∀y)[
(¬va(x) ∨ dz(x))  ∧
(¬dz(y) ∨ pr (y)) ∧
va(j)  ∧
¬pr (j)]


1. ¬va(x)   dz(x)
2. ¬dz(y)   pr (y)
3. va(j) 
4. ¬pr (j)]

5. (1, 3) x--> j
   dz(j)

6. (4, 2) y --> j
   ¬dz(j)


7. (5, 6)
   prazna klauza
  

----------------------------------------------------------------------------------------------------------------------

10. leti i lagano

 (R1 ∧ R2) ⇒ R3 treba pokazati da je ova formula valjana

 uzmemo negaciju formule i metodom rezolucije pokazemo da
 je negacija kontradiktorna

	
  ¬[(R1 ∧ R2) ⇒ R3]
  ¬[¬(R1 ∧ R2) ∨ R3]
	R1 ∧ R2 ∧ ¬R3


(∀x)(l(x) ⇒ (k(x) ∧ lag (x))) ∧
(∀x)(p(x) ⇒ ¬k(x)) ∧
¬(∀x)(p(x) ⇒ ¬l(x))

vesti na klauzalnu formu, prvo na Prenex

(∀x)(¬l(x) ∨ (k(x) ∧ lag (x))) ∧
(∀x)(¬p(x) ∨ ¬k(x)) ∧
¬(∀x)(¬p(x) ∨ ¬l(x))


dve stvari radimo:
u prvoj zagradi pravimo klauze
ulazimo negacijom u trecu recenicu

a ∨ (b ∧ c) --> (a ∨ b) ∧ (a ∨ c)



(∀x)((¬l(x) ∨ k(x)) ∧ (¬l(x) ∨ lag (x))) ∧
(∀x)(¬p(x) ∨ ¬k(x)) ∧
(∃x)(p(x) ∧ l(x))


radimo preimenovanje promenljivih (supstituciju)

(∀x1)((¬l(x1) ∨ k(x1)) ∧ (¬l(x1) ∨ lag (x1))) ∧
(∀x2)(¬p(x2) ∨ ¬k(x2)) ∧
(∃x3)(p(x3) ∧ l(x3))


sad izvlacimo kvantifikatore
i radi lakseg rada, povoljnije je prvo izvuci ∃
nije bitan redosled za ∀


(∃x3)(∀x1)(∀x2)[
   (¬l(x1) ∨ k(x1)) ∧
   (¬l(x1) ∨ lag (x1)) ∧
   (¬p(x2) ∨ ¬k(x2)) ∧
   p(x3) ∧
   l(x3)]

oslobadjamo se ∃ (skolemizacija)

x3 --> c (konstanta)

(∀x1)(∀x2)[
   (¬l(x1) ∨ k(x1)) ∧
   (¬l(x1) ∨ lag (x1)) ∧
   (¬p(x2) ∨ ¬k(x2)) ∧
   p(c) ∧
   l(c)]

sad mozemo da primenimo metod rezolucije

1. ¬l(x1)  k(x1)
2. ¬l(x1)  lag (x1)
3. ¬p(x2)  ¬k(x2)
4. p(c)
5. l(c)


6. (4, 3)  x2 --> c
           (ovu unifikaciju radimo da bi ¬p(x2)
            i p(c) mogli da se potiru)
           NE MOZE c --> x2 jer je c konstanta
    
    ¬k(c)


7. (6, 1) x1 --> c
    ¬l(c)


8. (7, 5)
		prazna klauza (kvadratic)


----------------------------------------------

5.  rodjaci, more i planina
      (u slajdovima greska kod trece renice, treba ∀, umesto ∃)


   -- treba pokazati da je skup ovih recenica kontradiktoran


   R1  ∧ R2 ∧ R3 ∧ R4 je kontradiktorna formula


(∀x)(rm(x) ∨ rp(x)) ∧
(∀x)(rm(x) ⇒ m(x)) ∧
(∀x)(rp(x) ⇒ p(x)) ∧
(∃x)(¬m(x) ∧ ¬p(x))


(∀x)(rm(x) ∨ rp(x)) ∧
(∀x)(¬rm(x) ∨ m(x)) ∧
(∀x)(¬rp(x) ∨ p(x)) ∧
(∃x)(¬m(x) ∧ ¬p(x))


preimenovanje promenljivih


(∀x1)(rm(x1) ∨ rp(x1)) ∧
(∀x2)(¬rm(x2) ∨ m(x2)) ∧
(∀x3)(¬rp(x3) ∨ p(x3)) ∧
(∃x4)(¬m(x4) ∧ ¬p(x4))


izvlacenje kvantifikatora

(∃x4)(∀x1)(∀x2)(∀x3)[
   (rm(x1) ∨ rp(x1)) ∧
   (¬rm(x2) ∨ m(x2)) ∧
   (¬rp(x3) ∨ p(x3)) ∧
   ¬m(x4) ∧ 
	 ¬p(x4)]


oslobadjamo se ∃ (kolemizacija)

x4 --> c

(∀x1)(∀x2)(∀x3)[
   (rm(x1) ∨ rp(x1)) ∧
   (¬rm(x2) ∨ m(x2)) ∧
   (¬rp(x3) ∨ p(x3)) ∧
   ¬m(c) ∧ 
	 ¬p(c)]


1. rm(x1)  rp(x1)
2. ¬rm(x2)  m(x2)
3. ¬rp(x3) ∨ p(x3)
4. ¬m(c)
5. ¬p(c)


6. (5, 3) x3 --> c
   ¬rp(c)

7. (4, 2) x2 --> c
   ¬rm(c)

8. (6, 1) x1 --> c
	 rm(c)

9. (8, 7)
   prazna klauza

-------------------------------------------------

4. braca

   R1  ∧ R2 ∧ R3 ∧ R4 je kontradiktorna formula   


(∀x)(∀y )(∃z)(b(x, y ) ⇒ (r (z, x) ∧ r (z, y ))) ∧
(∀x)(∀y )(r (x, y ) ⇒ s(x, y )) ∧
(∃x)(∃y )b(x, y ) ∧
(∀x)(∀y )¬s(x, y )



(∀x)(∀y )(∃z)(¬b(x, y ) ∨ (r (z, x) ∧ r (z, y ))) ∧
(∀x)(∀y )(¬r (x, y ) ∨ s(x, y )) ∧
(∃x)(∃y )b(x, y ) ∧
(∀x)(∀y )¬s(x, y )



(∀x)(∀y )(∃z)
  ((¬b(x, y ) ∨ r (z, x)) ∧ (¬b(x, y ) ∨ r (z, y ))) ∧
(∀x)(∀y )(¬r (x, y ) ∨ s(x, y )) ∧
(∃x)(∃y )b(x, y ) ∧
(∀x)(∀y )¬s(x, y )


preimenovanje promenljivih


(∀x1)(∀y1 )(∃z)
   ((¬b(x1, y1 ) ∨ r (z, x1)) ∧ 
    (¬b(x1, y1 ) ∨ r (z, y1 ))) ∧
(∀x2)(∀y2 )(¬r (x2, y2 ) ∨ s(x2, y2 )) ∧
(∃x3)(∃y3 )b(x3, y3 ) ∧
(∀x4)(∀y4 )¬s(x4, y4 )


izvlacimo kvantifikatore
idelano prvo ide ∃
(mora da se vodi racuna o redosledu i ∃ koje je iza ∀ mora da ostane iza)


(∃x3)(∃y3 )(∀x1)(∀y1 )(∃z)(∀x2)(∀y2 )(∀x4)(∀y4 )[
   (¬b(x1, y1 ) ∨ r (z, x1)) ∧
   (¬b(x1, y1 ) ∨ r (z, y1 )) ∧
   (¬r (x2, y2 ) ∨ s(x2, y2 )) ∧
   b(x3, y3 ) ∧
   ¬s(x4, y4 )]


oslobadjamo se ∃

x3 --> c1
y3 --> c2
z -->  f(x1, y1) ((∃z) iza je (∀x1)(∀y1 ) i zbog toga ne moze u konstantu vec mora u funkciju)


(∀x1)(∀y1 )(∀x2)(∀y2 )(∀x4)(∀y4 )[
   (¬b(x1, y1 ) ∨ r (f(x1, y1), x1)) ∧
   (¬b(x1, y1 ) ∨ r (f(x1, y1), y1 )) ∧
   (¬r (x2, y2 ) ∨ s(x2, y2 )) ∧
   b(c1, c2 ) ∧
   ¬s(x4, y4 )]


sad moze metod rezolucije

1. ¬b(x1, y1 )   r (f(x1, y1), x1)
2. ¬b(x1, y1 )   r (f(x1, y1), y1 )
3. ¬r (x2, y2 )  s(x2, y2 )
4. b(c1, c2 )
5. ¬s(x4, y4 )

6. (5, 3) x2 --> x4 (moze i obrnuto)
   ¬r (x4, y4 )


7. (6, 1)  x4 --> f(x1, y1)
               NE MOZE f(x1, y1) --> x4
           y4 --> x1
   ¬b(x1, y1 )


8. (7, 4) x1 --> c1
          y1 --> c2

   prazna klauza