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...
Main Author: | |
---|---|
Other Authors: | |
Language: | en |
Published: |
2014
|
Subjects: | |
Online Access: | http://www.theses.fr/2014PA112059/document |