Rozhodovacie postupy: Algoritmické hľadisko

Recenzie čitateľov

Momentálne nie sú žiadne recenzie čitateľov. Hodnotenie je založené na 12 hlasoch.

Pôvodný názov:

Decision Procedures: An Algorithmic Point of View

Obsah knihy:

Rozhodovacia procedúra je algoritmus, ktorý pri zadaní rozhodovacieho problému končí správnou odpoveďou áno/nie. Autori sa tu zameriavajú na teórie, ktoré sú dostatočne expresívne na to, aby modelovali reálne problémy, ale zároveň sú stále rozhodnuteľné.

Konkrétne sa kniha zameriava na rozhodovacie procedúry pre teórie prvého rádu, ktoré sa bežne používajú v automatizovanej verifikácii a zdôvodňovaní, v overovaní tvrdení, optimalizácii kompilátorov a operačnom výskume. Techniky opísané v knihe vychádzajú z oblastí, ako je teória grafov a logika, a bežne sa používajú v priemysle. Autori uvádzajú základnú terminológiu teórií modulov splniteľnosti a potom v samostatných kapitolách študujú rozhodovacie postupy pre každú z týchto teórií: výroková logika rovnosti a neinterpretované funkcie lineárna aritmetika bitové vektory polia ukazovacia logika a kvantifikované formuly.

Skúmajú aj problém rozhodovania kombinovaných teórií a jednu kapitolu venujú moderným technikám založeným na súhre riešiteľa SAT a rozhodovacej procedúry pre skúmanú teóriu. Táto učebnica sa používa na výučbu bakalárskych a magisterských kurzov na ETH v Zürichu, na Technione v Haife a na Oxfordskej univerzite.

Každá kapitola obsahuje podrobnú bibliografiu a cvičenia. Prezentácie pre prednášajúcich a knižnica C++ na rýchle prototypovanie rozhodovacích postupov sú k dispozícii na webovej stránke autorov.