Rozhodovací postupy: Algoritmické hledisko

Recenze čtenářů

Aktuálně nejsou k dispozici žádné recenze čtenářů. Hodnocení je založeno na 12 hlasů.

Původní název:

Decision Procedures: An Algorithmic Point of View

Obsah knihy:

Rozhodovací procedura je algoritmus, který při zadání rozhodovacího problému končí správnou odpovědí ano/ne. Autoři se zde zaměřují na teorie, které jsou dostatečně expresivní, aby modelovaly reálné problémy, ale přitom jsou rozhodovatelné.

Konkrétně se kniha zaměřuje na rozhodovací procedury pro teorie prvního řádu, které se běžně používají v automatické verifikaci a argumentaci, při dokazování teorémů, optimalizaci překladačů a operačním výzkumu. Techniky popsané v knize vycházejí z oborů, jako je teorie grafů a logika, a jsou běžně používány v průmyslu. Autoři uvádějí základní terminologii teorií splnitelnosti modulů a poté v samostatných kapitolách studují rozhodovací postupy pro každou z následujících teorií: výroková logika rovnosti a neinterpretované funkce lineární aritmetika bitové vektory pole ukazatelová logika a kvantifikované formule.

Studují také problém rozhodování kombinovaných teorií a jednu kapitolu věnují moderním technikám založeným na souhře SAT řešiče a rozhodovací procedury pro zkoumanou teorii. Tato učebnice byla použita při výuce v bakalářských a magisterských kurzech na ETH v Curychu, na Technionu v Haifě a na Oxfordské univerzitě.

Každá kapitola obsahuje podrobnou bibliografii a cvičení. Prezentace pro lektory a knihovna C++ pro rychlé prototypování rozhodovacích procedur jsou k dispozici na webových stránkách autorů.