Ocena:
Obecnie brak opinii czytelników. Ocena opiera się na 2 głosach.
Computational Logic and Set Theory: Applying Formalized Logic to Analysis
W miarę jak oprogramowanie komputerowe staje się coraz bardziej złożone, pytanie o to, w jaki sposób można zapewnić jego poprawność, staje się coraz bardziej krytyczne. Logika formalna zawarta w programach komputerowych jest ważną częścią odpowiedzi na ten problem.
Ten obowiązkowy tekst przedstawia pionierską pracę nieżyjącego już profesora Jacoba (Jacka) T. Schwartza nad logiką obliczeniową i teorią zbiorów oraz jej zastosowaniem w technikach weryfikacji dowodów, której kulminacją jest system tnaNova, prototypowy program komputerowy zaprojektowany do weryfikacji poprawności dowodów matematycznych przedstawionych w języku teorii zbiorów. Przyjmując systematyczne podejście, książka rozpoczyna się od przeglądu tradycyjnych gałęzi logiki, a następnie szczegółowo opisuje projekt systemu tnaNova. System ten jest następnie wykorzystywany do wyprowadzenia kilku głównych klasycznych wyników dotyczących nierozstrzygalności i nierozstrzygalności. Czytelnicy nie muszą posiadać dużej wiedzy z zakresu logiki formalnej, aby podążać za tekstem, chociaż zakłada się dobre zrozumienie standardowych technik programowania oraz znajomość matematyki definicji i scenariuszy dowodowych.
Tematy i cechy: z przedmową dr. Martina Davisa, emerytowanego profesora Courant Institute of Mathematical Sciences na Uniwersytecie Nowojorskim; dogłębnie opisuje, w jaki sposób można wykorzystać konkretną teorię pierwszego rzędu do modelowania i przeprowadzania rozumowań w gałęziach informatyki i matematyki; przedstawia unikalny system do automatycznej weryfikacji dowodów w systemach oprogramowania na dużą skalę; integruje ważne kwestie inżynierii dowodowej, odzwierciedlając cele weryfikatorów na dużą skalę; zawiera dodatek przedstawiający sformalizowane dowody rzędnych, różnych właściwości operacji domknięcia przechodniego, zasad indukcji skończonej i nieskończonej oraz lematu Zorna.
Ta przełomowa praca jest niezbędną lekturą dla badaczy i zaawansowanych absolwentów informatyki.
