Proceduri decizionale: Un punct de vedere algoritmic

Recenzii ale cititorilor

În prezent, nu există recenzii ale cititorilor. Evaluarea se bazează pe 12 voturi.

Titlul original:

Decision Procedures: An Algorithmic Point of View

Conținutul cărții:

O procedură de decizie este un algoritm care, dată fiind o problemă de decizie, se termină cu un răspuns corect da/nu. Aici, autorii se concentrează asupra teoriilor care sunt suficient de expresive pentru a modela probleme reale, dar care sunt totuși decidabile.

În mod specific, cartea se concentrează asupra procedurilor de decizie pentru teoriile de ordinul întâi care sunt utilizate în mod obișnuit în verificarea și raționamentul automatizat, demonstrarea teoremelor, optimizarea compilatoarelor și cercetarea operațională. Tehnicile descrise în carte se inspiră din domenii precum teoria grafurilor și logica și sunt utilizate în mod curent în industrie. Autorii introduc terminologia de bază a teoriilor modulo de satisfiabilitate și apoi, în capitole separate, studiază procedurile de decizie pentru fiecare dintre următoarele teorii: logică propozițională egalități și funcții neinterpretate aritmetică liniară vectori de biți matrice logică de pointer și formule cuantificate.

Ei studiază, de asemenea, problema deciziei teoriilor combinate și dedică un capitol tehnicilor moderne bazate pe o interacțiune între un rezolvator SAT și o procedură de decizie pentru teoria investigată. Acest manual a fost folosit pentru a preda cursuri de licență și de masterat la ETH Zurich, la Technion, Haifa, și la Universitatea din Oxford.

Fiecare capitol include o bibliografie detaliată și exerciții. Diapozitivele lectorilor și o bibliotecă C++ pentru prototiparea rapidă a procedurilor de decizie sunt disponibile pe site-ul web al autorilor.