Raisonnement automatisé : vérification formelle avec LISA

Cette séance de cours présente le laboratoire de raisonnement et d'analyse automatisés, en mettant l'accent sur la vérification formelle à l'aide de l'assistant d'épreuve LISA. Parmi les sujets abordés, mentionnons les épreuves mathématiques formelles, les assistants aux épreuves comme Coq et Isabelle, et les travaux récents sur le vérificateur d'équivalence de l'OCBSL. La séance de cours couvre le développement de LISA dans Scala, son application dans la logique, la théorie de l'ensemble et l'exactitude du programme, et l'algorithme pour vérifier l'équivalence des formules de proposition. On discute de la décidabilité du problème du mot OCBSL dans le temps log-linéaire et de la réduction à la forme normale, en soulignant son efficacité et sa prévisibilité dans la pratique.