Induction pour les solvants SMT

Cette séance de cours couvre les techniques d'induction dans les solveurs de Modulo Theories (SMT) Satisfiabilité, en mettant l'accent sur la mise en œuvre dans CVC4. Il examine les défis auxquels sont confrontés les résolveurs SMT dans le traitement des formules quantifiées et l'importance du raisonnement inductif. La séance de cours présente des exemples de conjectures au sol et quantifiées, soulignant la nécessité d'un renforcement inductif. Il explique le concept de génération de sous-objectifs dans le SMT, y compris la génération et le filtrage des sous-objectifs nécessaires. La séance de cours se termine par une discussion sur les benchmarks, les encodages et les résultats des solveurs SMT, soulignant la performance compétitive de CVC4 avec d'autres proverbes théorèmes inductifs.