Resavanje problema automatskog rasudjivanja Flashcards
(7 cards)
Sta sve spada u probleme automatskog rasudjivanja
Ove tehnike koristimo kada je potrebno netrivijalno rigorozno zakljucivanje. Tu spadaju i problemi u okviru kojih je potrebno dokazati da neko tvrdjenje vazi za sve moguce objekte koji zadovoljavaju neke preduslove, kao i problemi u okviru kojih je potrebno dokazati da postoje objekti za koje neko tvrdjenje vazi.
Faza resavanja problema u okviru automatskog rasudjivanja
- Modelovanje
2.Resavanje problema opisanog u matematickim terminima
3.interpretiranje i analiza resenja
Modelovanje problema
Modelovanje problema predstavlja formulisanje problema precizno, u matematickim terminima, koriscenjem pogodnog logickog okvira. Potrebno je najpre utvrditi vrstu osnovnih objekata i nepoznatih velicina u problemu. Onda treba opisati uslove koji moraju da vaze za objekte opisane u problemu.
Resavanje problema
U fazi resavanja problema, trazi se resenje matematicki formulisanog problema , koriscenjem pogodnih metoda zakljucivanje. Koriste se pametne metode (lenjo iracunavanje itd…)
Interpretiranje i analiza resenja
Dobijeno resenje matematicki formulisanog problema potrebno je formulisati u terminima pocetnog problema i potrebno je razumeti svojstva dobijenog resenja.
Zakljucci koji se dobijaju procesom resavanja su nesumnjivi, oni ne mogu biti pogrseni.
Najvaznije osobine algoritama za rasudjivanje
1.Potpunost = je svojstvo koje kaze da je algoritam u stanju da dokaze svako tvrdjene iz svog domena koje je tacno
2.Saglasnost= je svojstvo koje kaze da ako algoritam tvrdi da je neko tvrdjenje tacno onda ono zaista jeste tacno
Potpunost je pozeljna osobina,dok je saglasnost neophodna.
Sta su poluodlucivi problemi
Oni nisu odlucivi ali za njih moze da postoji algoritam koji moze da resi problem za sve instance na koje je odgovor “da”,ali za instance ciji je odgovor “ne” se ne zaustavlja .Jedan od takvih problema je halting problem
