mod Ex04 logic: 'cl'

rem 
  \para \bf  4. CVIĦENIE Z PREDMETU LOGIKA PRE INFORMATIKOV 2  \end 
  \para* http://ii.fmph.uniba.sk/cl/courses/lpi2/ex/ex04.cl 

rem 
  \para* \it  D÷tum:  \end ŷtvrtok 14. 10. 2004 
  \para* \it  Odporúīan÷ verzia CL:  \end 5.81.16 
  \para* \it  WWW str÷nka predmetu:  \end 
  http://ii.fmph.uniba.sk/cl/courses/lpi2?lang=sk 
  \para* \it  Kontakt na cviīiaceho:  \end mailto:kluka@fmph.uniba.sk 

rem 
  \para Preskoīte nasledujúce komponenty aŵ po nadpis "Logické problémy v 
  logike prvého r÷du". 

appldisp/0 Tau1
  Subsup(Id(0,Ent('tau'),0),75,Num('1',0),None)

appldisp/0 Taun
  Subsup(Id(0,Ent('tau'),0),75,Id(1,'n',0),None)

appldisp/2 Sa_boji_d
  Infix(Arg(0),25,1,Id(1,'sa bojí',0),Arg(1))

appldisp/2 Hates_d
  Infix(Arg(0),25,1,Id(1,'hates',0),Arg(1))

appldisp/2 Killed_d
  Infix(Arg(0),25,1,Id(1,'killed',0),Arg(1))

appldisp/2 Richer_d
  Infix(Arg(0),25,1,Id(1,'is richer than',0),Arg(1))

appldisp/1 Rich_d
  Postfix(Arg(0),25,0,Id(1,'is rich',0))

appldisp/1 Honest_d
  Postfix(Arg(0),25,0,Id(1,'is honest',0))

appldisp/1 Richx_d
  Postfix(Arg(0),25,0,Id(4,'is rich',0))

appldisp/1 Honestx_d
  Postfix(Arg(0),25,0,Id(4,'is honest',0))

appldisp/1 Not_d
  Prefix(24,2,Id(4,'not',0),Arg(0))

appldisp/2 Or_d
  Infix(Arg(0),22,1,Id(4,'or',0),Arg(1))

appldisp/2 And_d
  Infix(Arg(0),23,1,Id(4,'and',0),Arg(1))

appldisp/1 True_d
  Postfix(Fenced(Op(Ent('ldquo'),0),Arg(0),Op(Ent('rdquo'),0)),25,0,Id(1,'is true',0))

appldisp/2 Says_d
  Infix(Arg(0),25,1,Id(1,'says',0),
        Fenced(Op(Ent('ldquo'),0),Arg(1),Op(Ent('rdquo'),0)))

rem 
  \para \bf  Logické problémy v kvantifikaīnej logike (logike prvého r÷du). 
   \end 

rem 
  \para \bf  Som Drakula?  \end 
  \para Nasledujúca úvaha môŵe vyzeraš prekvapujúco: 
  \items 
   \item \para Kaŵdý sa bojí Drakulu. 
   \item \para Drakula sa bojí iba mňa. 
   \item \para Takŵe som Drakula. 
  \end
  \para Dok÷ŵte, ŵe je spr÷vna. 

rem 
  \para \it  Formaliz÷cia.  \end Predpoklady uvedeného tvrdenia sformalizujeme 
  pomocou axióm nasledujúcej teórie \ft O_drakulovi \end. Na formaliz÷ciu 
  potrebujeme dve konŷtanty -- \ft Drakula \end a \ft Ja \end-- a bin÷rny 
  predik÷t \ft Sa_boji \end zobrazovaný ako \ft Sa_boji_d(x,y) \end. 
  \para Vetu "Kaŵdý sa bojí Drakulu." zapíŷeme formulou 
  \eq (Ax1)
    \a xSa_boji_d(x,Dracula)
  \end
  \para Vetu "Drakula sa bojí iba mňa." môŵeme preformulovaš na "Vŷetci, 
  ktorých sa Drakula bojí, sú ja.", īo v jazyku logiky prvého r÷du 
  zapíŷeme ako 
  \eq (Ax2)
    \a x(Sa_boji_d(Dracula,x) -> x = Ja)
  \end
  \para Vaŷou úlohou je dok÷zaš tvrdenie "Som Drakula", teda 
  \eq (Som_drakula)
    Ja = Drakula
  \end
  \para Dokazovaī CL je v celom tomto cviīení v móde "first-order logic with 
  automatic rules". V tomto móde dokazovaī automaticky prenexuje formuly (teda 
  prepisuje ich podĵa pravidiel z druhej īasti Ex03) a umoŵňuje pouŵívaš 
  príkaz \bf  use  \end vo forme \bf  use  \end \ft Ax \end; \ft Tau1 \end; 
  ...; \ft Taun \end, ktor÷ pouŵije axiómu \ft Ax \end a z÷roveň ju 
  inŷtancuje dosadením \ft Tau1 \end,..., \ft Taun \end za vŷeobecne 
  kvantifikované premenné. 

theory O_drakulovi logic: 'fol_def'

fun/0 Drakula 

fun/0 Ja 

pred/2 Sa_boji 'Sa_boji_d'

axiom Ax1
  \a xSa_boji(x,Drakula)

axiom Ax2
  \a x(Sa_boji(Drakula,x) -> x = Ja)

thm Som_drakula
  Ja = Drakula
proof 
 use Ax1; Drakula
  use Ax2; Drakula proved...

end theory O_drakulovi

rem 
  \para Aby sme sa vyhli neobratným formul÷ci÷m ako "nenen÷vidí", zadanie 
  nasledujúceho problému uv÷dzame v angliītine. 

rem 
  \para \bf  Who killed Aunt Agatha?  \end 
  \para Someone who lives in Dreadbury Mansion killed Aunt Agatha. Agatha, the 
  butler, and Charles live in Dreadbury Mansion, and are the only people who 
  live therein. A killer always hates his victim, and is never richer than his 
  victim. Charles hates no one that Aunt Agatha hates. Agatha hates everyone 
  except the butler. The butler hates everyone not richer than Aunt Agatha. The 
  butler hates everyone Aunt Agatha hates. No one hates everyone. Agatha is not 
  the butler. Who killed Aunt Agatha? 

rem 
  \para \it  Formaliz÷cia.  \end Problém sme sformalizovali v teórii 
  \ft Agathas_killer \end. Vaŷou úlohou je dok÷zaš tvrdenie 
  \eq* 
    Killed_d(x,Agatha)
  \end
  \para* znamenajúce, ŵe \ft x \end (za ktoré \it  dosadíte  \end jednu z 
  troch konŷt÷nt z teórie) je vrahom tety Ag÷ty. 
  \para Porozmýŷĵajte nad vz÷jomnými vzšahmi jednotlivých osôb a 
  pokúste sa o nich dok÷zaš pomocné tvrdenia. Z nich potom dok÷ŵte hlavné 
  tvrdenie. Dok÷zané tvrdenie môŵete pouŵiš v Ĭalŷom dôkaze príkazom 
  \bf  use  \end podobne ako axiómu. Konŷtruujte pomocné tvrdenia a dôkazy 
  tak, aby īo najlepŷie odr÷ŵali úvahy, ktorými ste dospeli k rieŷeniu. 

theory Agathas_killer logic: 'fol_def'

pred Lives 'Lives_d'

pred/2 Hates 'Hates_d'

pred/2 Killed 'Killed_d'

pred/2 Richer 'Richer_d'

fun/0 Agatha 

fun/0 Charles 

fun/0 Butler 

axiom A1
  Lives(x) <-> x = Agatha \/ x = Butler \/ x = Charles

axiom A2
  \e x(Killed(x,Agatha) & Lives(x))

axiom A3
  Killed(x,y) -> Hates(x,y)

axiom A4
  Killed(x,y) -> ~Richer(x,y)

axiom A5
  Hates(Agatha,x) -> ~Hates(Charles,x)

axiom A6
  x != Butler -> Hates(Agatha,x)

axiom A7
  ~Richer(x,Agatha) -> Hates(Butler,x)

axiom A8
  Hates(Agatha,x) -> Hates(Butler,x)

axiom A9
  ~\e x(Lives(x) & \a y(Lives(y) -> Hates(x,y)))

axiom A10
  Agatha != Butler

thm Thm1
  Hates(Butler,Agatha)
proof 
 use A10
  use A6; Agatha
   use A8; Agatha proved....

thm Thm2
  ~Killed(Charles,Agatha)
proof 
 inv* ~Killed(Charles,Agatha)
  use A3; Charles; Agatha
   use A6; Agatha
    use A10
     use A5; Agatha proved......

thm Thm3
  Killed(x,Agatha) -> Hates(Butler,x)
proof 
 use A4; x; Agatha
  use A7; x proved...

thm Thm4
  Charles != Butler
proof 
 use A6; Agatha
  use A10
   use A5; Agatha
    use Thm1
     inv* Charles != Butler proved......

thm Thm5
  Hates(Agatha,Charles)
proof 
 use A6; Charles
  use Thm4 proved...

thm Thm6
  ~Hates(Butler,Butler)
proof 
 use Thm1
  use Thm5
   use A8; Charles
    inv* ~Hates(Butler,Butler)
     use A9.0:0; Butler
      use A1.0; Butler
       inv ~\a y(Lives(y) -> Hates(Butler,y))
        eigen* \a y(Lives(y) -> Hates(Butler,y)).0; y
         use A1.0; y
          split y = Agatha \/ y = Butler \/ y = Charles.4,0,0,0,0
           proved
           proved
           proved...........

thm Thm7
  ~Killed(Butler,Agatha)
proof 
 use Thm3; Butler
  use Thm6 proved...

thm Agatha_commited_suicide
  Killed(Agatha,Agatha)
proof 
 use A2.0
  eigen \e x(Killed(x,Agatha) & Lives(x)).0; x
   use A1.0; x
    use Thm2
     use Thm7
      split x = Agatha \/ x = Butler \/ x = Charles.4,0,0,0,0
       proved
       proved
       proved.......

end theory Agathas_killer

rem 
  \para \bf  O poctivcoch, klam÷roch a presviedīaní.  \end 
  \items 
   \item \para Na jednom vzdialenom ostrove ŵijú zvl÷ŷtni ĵudia. Kaŵdý je 
         buĬ poctivec (vŵdy hovorí pravdu) alebo klam÷r (vŵdy hovorí 
         nepravdu) a bohatý alebo chudobný. 
   \item \para Aké tvrdenie m÷ zvoliš bohatý klam÷r, aby presvedīil 
         dievīa, do ktorého sa zamiloval, ŵe je bohatým klam÷rom? 
  \end

rem 
  \para \it  Formaliz÷cia.  \end \header* pred/2 Says  \end 
  \header* fun/2 Andx  \end \header* fun/2 Orx  \end 
  \items 
   \item \para Predik÷t \ft Honest(x) \end ( \ft Honest_d(x) \end) platí, ak 
         \ft x \end je poctivec. 
   \item \para Predik÷t \ft ~Honest(x) \end ( \ft ~Honest_d(x) \end) platí, ak 
         \ft x \end je klam÷r. 
   \item \para Predik÷t \ft Rich(x) \end ( \ft Rich_d(x) \end) platí, ak 
         \ft x \end je bohatý. 
   \item \para Predik÷t \ft ~Rich(x) \end ( \ft ~Rich_d(x) \end) platí, ak 
         \ft x \end je chudobný. 
   \item \para Predik÷t \ft True(a) \end ( \ft True_d(a) \end) platí, ak 
         tvrdenie \ft a \end platí. 
   \item \para Tvrdenie \ft a \end sa vytv÷ra pomocou funkīných symbolov: 
         \items 
          \item \para \ft Honestx(x) \end ( \ft Honestx_d(a) \end) symbolizuje 
                \ft Honest(x) \end, 
          \item \para \ft Richx(x) \end ( \ft Richx_d(a) \end) symbolizuje 
                \ft Rich(x) \end, 
          \item \para \ft Notx(a) \end ( \ft Not_d(a) \end) symbolizuje 
                \ft ~a \end, 
          \item \para \ft Andx(a,b) \end ( \ft And_d(a,b) \end) symbolizuje 
                \ft a & b \end, 
          \item \para \ft Orx(a,b) \end ( \ft Or_d(a,b) \end) symbolizuje 
                \ft a \/ b \end, 
         \end
         \para kde \ft a \end, \ft b \end sú tvrdenia. 
   \item \para Predik÷t \ft Says(x,a) \end ( \ft Says_d(x,a) \end) platí, ak 
         \ft a \end je tvrdenie, ktoré vie povedaš \ft x \end (poctivci vedia 
         povedaš iba pravdivé tvrdenia, klam÷ri iba nepravdivé). 
  \end
  \para Vaŷou úlohou je dok÷zaš 
  \eq (Problem)
    \e a(Says_d(x,a) <-> Rich_d(x) & ~Honest_d(x))
  \end
  \para teda n÷jsš také tvrdenie, ktoré \ft x \end vie povedaš pr÷ve 
  vtedy, keĬ je bohatým klam÷rom. 

theory Theory logic: 'fol_def'

pred Honest 'Honest_d'

pred Rich 'Rich_d'

fun Honestx 'Honestx_d'

fun Richx 'Richx_d'

fun Notx 'Not_d'

fun/2 Andx 'And_d'

fun/2 Orx 'Or_d'

pred True 'True_d'

pred/2 Says 'Says_d'

axiom Th
  True Honestx(x) <-> Honest(x)

axiom Tr
  True Richx(x) <-> Rich(x)

axiom Tn
  True Notx(a) <-> ~True(a)

axiom Ta
  True Andx(a,b) <-> True(a) & True(b)

axiom To
  True Orx(a,b) <-> True(a) \/ True(b)

axiom Sh
  Honest(x) -> Says(x,a) <-> True(a)

axiom Snh
  ~Honest(x) -> Says(x,a) <-> ~True(a)

thm Problem
  \e a(Says(x,a) <-> Rich(x) & ~Honest(x))

end theory Theory