Logica computațională și teoria seturilor: Aplicarea logicii formalizate la analiză

Recenzii ale cititorilor

În prezent, nu există recenzii ale cititorilor. Evaluarea se bazează pe 2 voturi.

Titlul original:

Computational Logic and Set Theory: Applying Formalized Logic to Analysis

Conținutul cărții:

Pe măsură ce programele informatice devin din ce în ce mai complexe, problema modului în care poate fi asigurată corectitudinea lor devine din ce în ce mai critică. Logica formală încorporată în programele de calculator este o parte importantă a răspunsului la această problemă.

Acest text obligatoriu de citit prezintă munca de pionierat a regretatului profesor Jacob (Jack) T. Schwartz în domeniul logicii computaționale și al teoriei seturilor, precum și aplicarea acestora la tehnicile de verificare a dovezilor, culminând cu sistemul tnaNova, un prototip de program de calculator conceput pentru a verifica corectitudinea dovezilor matematice prezentate în limbajul teoriei seturilor. Având o abordare sistematică, cartea începe cu o trecere în revistă a ramurilor tradiționale ale logicii, înainte de a descrie în detaliu proiectul care stă la baza sistemului tnaNova. Acest sistem este apoi utilizat pentru a deriva câteva dintre principalele rezultate clasice privind indecidabilitatea și nerezolvabilitatea. Cititorii nu au nevoie de cunoștințe mari de logică formală pentru a urmări textul, deși se presupune o bună înțelegere a tehnicilor standard de programare și o familiaritate cu matematica definițiilor și scenariilor de dovezi.

Subiecte și caracteristici: cu o prefață de dr. Martin Davis, profesor emerit al Institutului Courant de Științe Matematice, Universitatea din New York; descrie în profunzime modul în care o teorie specifică de ordinul întâi poate fi exploatată pentru a modela și a efectua raționamente în ramuri ale informaticii și matematicii; prezintă un sistem unic pentru verificarea automată a dovezilor în sisteme software la scară largă; integrează probleme importante de inginerie a dovezilor, reflectând obiectivele verificatorilor la scară largă; include o anexă care prezintă dovezi formalizate ale ordinalelor, ale diferitelor proprietăți ale operației de închidere tranzitivă, ale principiilor de inducție finite și transfinite și ale lemmei lui Zorn.

Această lucrare inovatoare este o lectură esențială pentru cercetători și absolvenți avansați de informatică.