Výpočetní logika a teorie množin: Vědecké přednášky: Aplikace formalizované logiky v analýze

Recenze čtenářů

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

Původní název:

Computational Logic and Set Theory: Applying Formalized Logic to Analysis

Obsah knihy:

S rostoucí složitostí počítačového softwaru je stále důležitější otázka, jak zajistit jeho správnost. Formální logika obsažená v počítačových programech je důležitou součástí odpovědi na tento problém.

Tento povinný text představuje průkopnickou práci zesnulého profesora Jacoba (Jacka) T. Schwartze v oblasti počítačové logiky a teorie množin a její aplikaci na techniky ověřování důkazů, která vyvrcholila systémem tnaNova, prototypem počítačového programu určeného k ověřování správnosti matematických důkazů prezentovaných v jazyce teorie množin. Kniha, která zaujímá systematický přístup, začíná přehledem tradičních odvětví logiky a poté podrobně popisuje základní konstrukci systému tnaNova. Tento systém je pak použit k odvození několika hlavních klasických výsledků o nerozhodnutelnosti a neřešitelnosti. Čtenáři ke sledování textu nepotřebují velké znalosti formální logiky, i když se předpokládá dobrá znalost standardních programovacích technik a znalost matematiky definic a důkazových scénářů.

Témata a vlastnosti: s předmluvou dr. Martina Davise, emeritního profesora Courantova institutu matematických věd na Newyorské univerzitě; podrobně popisuje, jak lze specifickou teorii prvního řádu využít k modelování a provádění úvah v oborech informatiky a matematiky; představuje unikátní systém pro automatizované ověřování důkazů v rozsáhlých softwarových systémech; integruje důležité otázky důkazového inženýrství, které odrážejí cíle rozsáhlých ověřovatelů; obsahuje přílohu ukazující formalizované důkazy ordinálů, různých vlastností operace tranzitivního uzávěru, principů konečné a transfinitní indukce a Zornova lemmatu.

Tato průkopnická práce je nezbytnou četbou pro výzkumné pracovníky a pokročilé absolventy informatiky.