Dynamická logika

Recenze čtenářů

Kniha podává podrobný výklad dynamické logiky a zpřístupňuje ji pro pochopení různých logických konstrukcí. Zdůrazňuje význam formální logiky v softwarovém inženýrství a její aplikace při uvažování o počítačových algoritmech.

⬤ Přehledný a ucelený výklad dynamické logiky.
⬤ Cenné poznatky o formální logice a jejím významu pro softwarové inženýry.
⬤ Pomáhá vytvořit základy pro pochopení rozšíření logiky, jako je modální a temporální logika.

⬤ Pro některé čtenáře může být kniha pouze úvodním krokem („předkrmem“), aniž by zacházela do pokročilých detailů.
⬤ Nezabývá se softwarem pro automatické uvažování, což by někteří čtenáři mohli očekávat.

(na základě 3 hodnocení čtenářů)

Původní název:

Dynamic Logic

Obsah knihy:

Tato kniha je prvním uceleným úvodem do dynamické logiky.

Mezi mnoha přístupy k formálnímu uvažování o programech má dynamická logika tu jedinečnou výhodu, že je silně spjata s klasickou logikou. Její varianty představují přirozená zobecnění a rozšíření klasických formalismů. Například výrokovou dynamickou logiku (PDL) lze popsat jako směs tří vzájemně se doplňujících klasických složek: výrokového kalkulu, modální logiky a algebry pravidelných událostí. V dynamické logice prvního řádu (DL) je výrokový kalkul nahrazen klasickým predikátovým kalkulem prvního řádu. Dynamická logika je systém pozoruhodné jednoty, který je teoreticky bohatý a má i praktickou hodnotu. Lze ji použít k formalizaci specifikací správnosti a k důslednému dokazování, že tyto specifikace jsou splněny konkrétním programem. Mezi další využití patří určování ekvivalence programů, porovnávání vyjadřovací schopnosti různých programovacích konstrukcí a syntéza programů ze specifikací.

Tato kniha je prvním uceleným úvodem do dynamické logiky. Je rozdělena do tří částí. První část podává přehled příslušných základních pojmů logiky a teorie vypočitatelnosti a může stát samostatně jako úvod do těchto témat. Druhá část pojednává o PDL a jejích variantách a třetí část o DL a jejích variantách. V celé knize jsou uvedeny příklady a na konci každé kapitoly jsou zařazena cvičení a krátká historická část.