Séance de cours
Cette séance de cours couvre les concepts de la Logique Second Order (SOL), de la Logique Second Order monadic faible et de la Logique Second Order monadic faible de 1 Successeur. Il explique la syntaxe et la sémantique des formules WS1S, des procédures de décision, des formules atomiques et composites, et la fonction d'intégration traduisant les formules WS1S en formules HOL. La séance de cours traite également de la combinaison de WS1S et MONA avec HOL et Isabelle, illustrant comment exprimer des problèmes dans HOL et résoudre automatiquement des sous-problèmes dans WS1S. La présentation se termine par l'utilisation de l'oracle, l'exactitude et les théorèmes liés à WS1S et HOL.