[Solomonov Seminar] 33. in 34. Solomonov seminar

[Marko Grobelnik]

Vabim vas na 33. in 34. Solomonov seminar, ki bosta
v ponedeljek (19.2.2001) in torek (20.2.2001)
obakrat ob 13h v sejni sobi E8 (IJS).

Prvi seminar (v ponedeljek) bo imel Andrej Bauer, ki je na
nekaj dnevnem obisku v Sloveniji, govoril pa bo o zanimivem
eksperimentu, pri katerem so na CMUju dokazovali, da ne
obstaja neodlocljivih enacb do dolzine 12 simbolov.

Drugi seminar (v torek) bo imel Mare Bohanec, kjer bo predstavil
3 programe s podrocja odlocitvene analize - gotovo zanimivo za vse,
ki bi radi izvedeli kaj vec o racunalniski podpori pri odlocanju.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Andrej Bauer:
               Ali so vsi kratki stavki odlocljivi?

Znameniti Gödelov izrek pravi, da obstajajo neodlocljivi stavki Peanove aritmetike. Oktobra 1999 je Harvey Friedman na obisku na CMU
vprasal, kako dolg je najkrajsi neodlocljiv stavek Peanove aritmetike. Postavil je hipotezo, da so vsi stavki krajsi od principa
matematicne indukcije bodisi dokazljivi bodisi ovrgljivi iz Peanovih aksiomov. Zanimivo je vprasanje, kako bi tako hipotezo
dokazali.
Princip matematicne indukcije lahko zapisemo z 12 znaki, pri cemer ne stejemo kvantifikatorjev in oklepajev:

  P(0) & (ALL x. P(x) --> P(s(x))) --> (ALL x. P(x))
Stevilo stavkov, ki so krajsi od 12 znakov, steje v miljone in ocitno je, da je to delo za racunalnike in avtomatske dokazovalnike.
Z Johnom Langfordom sva opravila prve poskuse v Mathematici in nato presedlala v programski jezik OCAML. Mathematica zna dobro
poenostavljati izraze in je bila zato prakticna na zacetku, a je prepocasna za resne poskuse na stavkih, ki so daljsi od 9 znakov.
Na seminarju bom predstavil prijeme iz simbolnega racuna in avtomatskega dokazovanja, ki sva jih uporabila. Poskus se ni koncan,
tako da ne vem, kaksen bo rezultat. Neuspeh lahko merimo s stevilom stavkov, ki jih racunalnik ni znal sam odlociti.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Marko Bohanec:
               Trije programi s podrocja odlocitvene analize

Odlocitvena analiza (Decision Analysis) je eden od bolj znanih pristopov, ki se
uporablja pri podpori zahtevnih odlocitvenih procesov. Temelji na sistematicni
analizi odlocitvenega problema in gradnji odlocitvenih modelov, kot so
odlocitvena drevesa, diagrami vpliva ali vecparametrski modeli. Taksni modeli se
potem uporabljajo za vrednotenje in vsestransko preucevanje moznih odlocitev ter
za izbor, razlago in utemeljitev najboljsih. Na seminarju bodo okvirno
predstavljeni trije novejsi racunalniski programi s tega podrocja: (1) DATA za
delo z odlocitvenimi drevesi, (2) Analytica za delo z diagrami vpliva ter (3)
DecisionPro za gradnjo splosnih racunskih modelov.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~