Avis des lecteurs
Il n'y a actuellement aucun avis de lecteur. La note est basée sur 2 votes.
Titre original :
Computational Logic and Set Theory: Applying Formalized Logic to Analysis
Contenu du livre :
Au fur et à mesure que les logiciels deviennent plus complexes, la question de savoir comment garantir leur exactitude devient de plus en plus cruciale. La logique formelle incorporée dans les programmes informatiques est un élément important de la réponse à ce problème.
Ce texte incontournable présente les travaux pionniers de feu le professeur Jacob (Jack) T. Schwartz sur la logique computationnelle et la théorie des ensembles, ainsi que leur application aux techniques de vérification des preuves, qui ont abouti au système tnaNova, un prototype de programme informatique conçu pour vérifier l'exactitude des preuves mathématiques présentées dans le langage de la théorie des ensembles. Adoptant une approche systématique, le livre commence par une étude des branches traditionnelles de la logique avant de décrire en détail la conception sous-jacente du système tnaNova. Ce système est ensuite utilisé pour dériver plusieurs des principaux résultats classiques sur l'indécidabilité et l'insolubilité. Les lecteurs n'ont pas besoin d'une grande connaissance de la logique formelle pour suivre le texte, bien qu'une bonne compréhension des techniques de programmation standard et une familiarité avec les mathématiques des définitions et des scénarios de preuve soient supposées.
Sujets et caractéristiques : avec un avant-propos du Dr. Martin Davis, professeur émérite du Courant Institute of Mathematical Sciences, New York University ; décrit en profondeur comment une théorie spécifique du premier ordre peut être exploitée pour modéliser et effectuer des raisonnements dans des branches de l'informatique et des mathématiques ; présente un système unique pour la vérification automatisée de preuves dans des systèmes logiciels à grande échelle ; intègre d'importantes questions d'ingénierie de la preuve, reflétant les objectifs des vérificateurs à grande échelle ; comprend une annexe montrant des preuves formalisées des ordinaux, de diverses propriétés de l'opération de fermeture transitive, des principes d'induction finie et transfinie, et du lemme de Zorn.
Cet ouvrage novateur est une lecture essentielle pour les chercheurs et les diplômés avancés en informatique.
Autres informations sur le livre :
| ISBN : | 9780857298072 |
| Auteur : | |
| Éditeur : | |
| Reliure : | Relié |
| Année de publication : | 2011 |
| Nombre de pages : | 416 |
Achat:
Actuellement disponible, en stock.
