|
Depot Institutionnel de l'UMBB >
Thèses de Doctorat et Mémoires de Magister >
Informatique >
Magister >
Veuillez utiliser cette adresse pour citer ce document :
http://dlibrary.univ-boumerdes.dz:8080/handle/123456789/888
|
| Titre: | Formalisation de la logique temporelle dans le coq |
| Auteur(s): | Belkacemi, Lila |
| Mots-clés: | Logique temporelle
Axiomatique
Coq (logiciel) |
| Date de publication: | 2014 |
| Résumé: | L'objectif de ce travail est de fournir une formalisation de la syntaxe ainsi que la sémantique de la logique temporelle linéaire propositionnelle(LTLP) en utilisant le langage de spécification GALLINA de l'assistant de preuves Coq. Par la suite, nous donnerons une vérification formelle de terminaison de l'algorithme du tableau sémantique por cette logique dans l'assistant de preuve Coq |
| URI/URL: | http://dlibrary.univ-boumerdes.dz:8080/jspui/handle/123456789/888 |
| Collection(s) : | Magister
|
Fichier(s) constituant ce document :
|
Tous les documents dans DSpace sont protégés par copyright, avec tous droits réservés.
|
