Ocena:
Obecnie brak opinii czytelników. Ocena opiera się na 12 głosach.
Decision Procedures: An Algorithmic Point of View
Procedura decyzyjna to algorytm, który, biorąc pod uwagę problem decyzyjny, kończy się poprawną odpowiedzią tak/nie. Autorzy skupiają się tutaj na teoriach, które są wystarczająco ekspresyjne, aby modelować rzeczywiste problemy, ale nadal są rozstrzygalne.
W szczególności, książka koncentruje się na procedurach decyzyjnych dla teorii pierwszego rzędu, które są powszechnie stosowane w automatycznej weryfikacji i wnioskowaniu, rozwiązywaniu twierdzeń, optymalizacji kompilatorów i badaniach operacyjnych. Techniki opisane w książce czerpią z takich dziedzin jak teoria grafów i logika i są rutynowo stosowane w przemyśle. Autorzy wprowadzają podstawową terminologię teorii zadowalalności modulo, a następnie, w osobnych rozdziałach, badają procedury decyzyjne dla każdej z następujących teorii: logika zdaniowa równości i funkcje nieinterpretowane arytmetyka liniowa wektory bitowe tablice logika wskaźnikowa i formuły kwantyfikatorowe.
Badają również problem rozstrzygania teorii kombinatorycznych i poświęcają rozdział nowoczesnym technikom opartym na współdziałaniu solwera SAT i procedury decyzyjnej dla badanej teorii. Podręcznik ten był wykorzystywany do prowadzenia kursów licencjackich i magisterskich w ETH Zurich, w Technion w Hajfie i na Uniwersytecie Oksfordzkim.
Każdy rozdział zawiera szczegółową bibliografię i ćwiczenia. Slajdy dla wykładowców i biblioteka C++ do szybkiego prototypowania procedur decyzyjnych są dostępne na stronie internetowej autorów.