Számítási logika és halmazelmélet: A formalizált logika alkalmazása az analízisben

Olvasói vélemények

Jelenleg nincsenek olvasói vélemények. Az értékelés 2 olvasói szavazat alapján történt.

Eredeti címe:

Computational Logic and Set Theory: Applying Formalized Logic to Analysis

Könyv tartalma:

Ahogy a számítógépes szoftverek egyre összetettebbé válnak, úgy válik egyre kritikusabbá a kérdés, hogy miként biztosítható a helyességük. A számítógépes programokban megtestesülő formális logika fontos része az erre a problémára adott válasznak.

Ez a kötelezően olvasandó szöveg bemutatja a néhai Jacob (Jack) T. Schwartz professzor úttörő munkásságát a számítógépes logika és halmazelmélet terén, valamint ezek alkalmazását a bizonyítási technikákhoz, amelynek csúcspontja a tnaNova rendszer, egy olyan számítógépes program prototípusa, amelyet a halmazelmélet nyelvén bemutatott matematikai bizonyítások helyességének ellenőrzésére terveztek. A könyv szisztematikus megközelítést alkalmazva a logika hagyományos ágainak áttekintésével kezdődik, mielőtt részletesen ismertetné a tnaNova rendszer alapjául szolgáló tervezést. Ezt követően ezt a rendszert használja a megdönthetetlenséggel és megoldhatatlansággal kapcsolatos számos fő klasszikus eredmény levezetésére. Az olvasónak nem kell nagyfokú ismeretekkel rendelkeznie a formális logikában ahhoz, hogy követni tudja a szöveget, bár a szabványos programozási technikák jó ismerete, valamint a definíciók és bizonyítási forgatókönyvek matematikájának ismerete feltételezhető.

Témák és jellemzők: előszóval dr. Martin Davis, a New York-i Egyetem Courant Matematikai Tudományok Intézetének emeritus professzora; részletesen leírja, hogyan lehet egy konkrét elsőrendű elméletet kihasználni az érvelés modellezésére és végrehajtására az informatika és a matematika ágaiban; bemutat egy egyedülálló rendszert a nagyméretű szoftverrendszerek automatizált bizonyításellenőrzéséhez; integrálja a bizonyítás-technika fontos kérdéseit, tükrözve a nagyméretű verifikátorok céljait; tartalmaz egy függeléket, amely formalizált bizonyításokat mutat be az ordinálisokról, a tranzitív zárási művelet különböző tulajdonságairól, a véges és transzfinit indukciós elvekről és a Zorn-lemmáról.

Ez az úttörő munka nélkülözhetetlen olvasmány a kutatók és az informatika felsőfokú végzettségűek számára.