Hodnotenie:
Momentálne nie sú žiadne recenzie čitateľov. Hodnotenie je založené na 2 hlasoch.
Computational Logic and Set Theory: Applying Formalized Logic to Analysis
So zvyšujúcou sa zložitosťou počítačového softvéru je otázka, ako zabezpečiť jeho správnosť, čoraz dôležitejšia. Formálna logika obsiahnutá v počítačových programoch je dôležitou súčasťou odpovede na tento problém.
Tento text, ktorý si musíte prečítať, predstavuje priekopnícku prácu zosnulého profesora Jacoba (Jacka) T. Schwartza v oblasti počítačovej logiky a teórie množín a jej aplikáciu na techniky overovania dôkazov, ktorá vyvrcholila systémom tnaNova, prototypom počítačového programu určeného na overovanie správnosti matematických dôkazov prezentovaných v jazyku teórie množín. Kniha sa začína systematickým prístupom, prehľadným prehľadom tradičných odvetví logiky, a potom sa podrobne opisuje základný návrh systému tnaNova. Tento systém sa potom používa na odvodenie niekoľkých hlavných klasických výsledkov o nerozhodnuteľnosti a neriešiteľnosti. Čitatelia na sledovanie textu nepotrebujú veľké znalosti formálnej logiky, hoci sa predpokladá dobrá znalosť štandardných programovacích techník a znalosť matematiky definícií a dôkazových scenárov.
Témy a vlastnosti: s predslovom dr. Martina Davisa, emeritného profesora Courant Institute of Mathematical Sciences, New York University; podrobne opisuje, ako možno špecifickú teóriu prvého rádu využiť na modelovanie a realizáciu uvažovania v odvetviach informatiky a matematiky; predstavuje unikátny systém na automatizovanú verifikáciu dôkazov vo veľkých softvérových systémoch; integruje dôležité otázky dôkazového inžinierstva, ktoré odrážajú ciele veľkých verifikátorov; obsahuje prílohu, v ktorej sú uvedené formalizované dôkazy ordinálov, rôznych vlastností operácie tranzitívneho uzáveru, princípov konečnej a nekonečnej indukcie a Zornovej lemy.
Táto prelomová práca je nevyhnutným čítaním pre výskumníkov a pokročilých absolventov informatiky.
