Príručka praktickej logiky a automatizovaného uvažovania

Recenzie čitateľov

Kniha je vysoko hodnotená pre svoj komplexný a praktický prístup k automatizovanému dokazovaniu tvrdení (ATP), najmä vďaka podrobnej implementácii v jazyku OCaml. Čitatelia oceňujú zrozumiteľnosť a radosť z písania, hoci existujú určité nedostatky týkajúce sa jej použitia ako referencie.

⬤ Vynikajúci úvod do automatizovaného dokazovania tvrdení s jasným postupom od základov k pokročilým témam.
⬤ Kompletné implementácie algoritmov v jazyku OCaml, čo zvyšuje prehľadnosť a pochopenie.
⬤ Príjemný štýl písania, ktorý robí tému pútavou.
⬤ Vhodný na vytvorenie vlastného automatizovaného dokazovania tvrdení od začiatku.
⬤ Považuje sa za povinnú výbavu pre tých, ktorí sa zaujímajú o automatizované rozhodovacie postupy.

⬤ Obmedzené pokrytie moderných riešiteľov SMT.
⬤ Použitie jazyka OCaml možno považovať za nevýhodu v porovnaní s používanejšími jazykmi, ako sú C++ alebo Java.
⬤ Môže byť časovo náročné vyhľadávať implementácie základných funkcií, ak sa kniha používa skôr ako referencia než ako učebnica.

(na základe 5 čitateľských recenzií)

Pôvodný názov:

Handbook of Practical Logic and Automated Reasoning

Obsah knihy:

Táto kniha spĺňa požiadavku na samostatný a rozsiahly opis koncepcií, mechanizmov a používania automatizovaného uvažovania.

Matematické základy logiky sú opísané v spojení s praktickým použitím, a to všetko s minimálnymi predpokladmi. Prístup je konštruktívny, konkrétny a algoritmický: kľúčovou črtou je, že metódy sú opísané s odkazom na skutočné implementácie (pre ktoré je uvedený kód), ktoré môžu čitatelia používať, upravovať a experimentovať s nimi.

Táto kniha je ideálna pre tých, ktorí hľadajú komplexný zdroj informácií o všeobecnej oblasti automatizovaného uvažovania. Možno ju použiť ako referenciu alebo ako miesto na osvojenie si základov, a to buď v spojení s pokročilými kurzami, alebo na samoštúdium.