Raisonnement équationnel et méthodes de combinaison: de la programmation à la preuve
Les travaux décrits dans ce document ont pour objectif le développement de procédures de décision (et de résolution) pour la vérification. La logique considérée est la logique du premier ordre avec égalité. Cette logique est évidemment indécidable en général, mais l'étude de fragments intéressa...
| Main Author: | |
|---|---|
| Language: | FRE |
| Published: |
Université Henri Poincaré - Nancy I
2009
|
| Subjects: | |
| Online Access: | http://tel.archives-ouvertes.fr/tel-00578600 http://tel.archives-ouvertes.fr/docs/00/57/86/00/PDF/uhp-hdr-cr.pdf |