Cette séance de cours couvre le problème de l'élimination des quantificateurs en arithmétique de Presbourg, en se concentrant sur la normalisation des littéraux, en exposant les variables à éliminer, en assurant les coefficients et en gérant les limites inférieures et supérieures. Il fournit également des exemples et discute de la complexité de décider des formules de PA quantifiées.