Procédures de décision génériques pour des théories axiomatiques du premier ordre

Les solveurs SMT sont des outils dédiés à la vérification d'un ensemble de formules mathématiques, en général sans quantificateurs, utilisant un certain nombre de théories prédéfinies, telles que la congruence, l'arithmétique linéaire sur les entiers, les rationnels ou les réels, les t...

Full description

Bibliographic Details
Main Author: Dross, Claire
Other Authors: Paris 11
Language:en
Published: 2014
Subjects:
Online Access:http://www.theses.fr/2014PA112059/document