Formal Logic: Classical Problems and Proofs
La logique consiste - sans aucun doute - à prouver, mais les preuves peuvent être "coûteuses", souvent de manière impossible, et aujourd'hui la plupart sont déléguées à des prouveurs (partiellement) automatiques, notamment par ce que l'on appelle les solveurs SAT, des logiciels basés sur le problème de la satisfiabilité (booléenne), ou SAT. Il s'agit du double du problème de validité (booléenne), ou VAL, qui est au cœur de la conception de l'ordinateur numérique via le Entscheidungsproblem de Hilbert et la machine de Turing universelle. Alors que ces problèmes - le VAL, bien moins que le SAT - figurent dans les manuels d'introduction à la logique destinés aux étudiants en informatique, ils sont largement ou totalement absents des manuels destinés aux étudiants en mathématiques ou en philosophie.
Formal logic : Classic problems and proofs corrige cet état de fait, à notre avis erroné, en fournissant les bases de la logique classique formelle du point de vue central d'un langage formel, ou informatique, qui se distingue des autres langages formels ou informatiques par sa capacité à préserver la vérité, fournissant ainsi potentiellement des solutions aux problèmes de décision formulés en termes de VAL et/ou de SAT. Cet aspect fondamental de la logique classique, la préservation de la vérité, est développé à partir de trois sémantiques formelles principales, à savoir la sémantique tarskienne, la sémantique de Herbrand et la sémantique algébrique (booléenne), qui, à leur tour, par le biais des résultats d'adéquation pour la logique standard du premier ordre, sous-tendent les principaux systèmes de preuves directes et indirectes, ou de réfutation, associés à VAL et SAT, respectivement.
Ne se concentrant pas sur l'histoire de la logique classique, ce livre fournit néanmoins des discussions et cite des passages centraux sur ses origines et son développement, notamment d'un point de vue philosophique. N'étant pas un livre de logique mathématique, il aborde la logique formelle d'un point de vue essentiellement mathématique. Orienté vers une approche computationnelle, avec SAT et VAL comme colonne vertébrale, il s'agit donc d'une introduction à la logique qui couvre les aspects essentiels des trois branches de la logique, à savoir philosophique, mathématique et computationnelle.
© Book1 Group - tous droits réservés.
Le contenu de ce site ne peut être copié ou utilisé, en tout ou en partie, sans l'autorisation écrite du propriétaire.
Dernière modification: 2024.11.14 07:32 (GMT)