Automatiser les preuves logiques de premier ordre en utilisant la résolution

Cette séance de cours présente la logique du premier ordre (FOL) comme un outil puissant pour formaliser les mathématiques et les problèmes de vérification de programme. Il couvre la syntaxe FOL, la sémantique et la procédure de résolution pour prouver les propriétés. L'instructeur explique les signatures FOL, les interprétations, la satisfaisabilité et la validité, illustrant ces concepts avec des exemples.