|
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/914
|
| Titre: | Un système de preuve d'ordre supérieure basé sur le E lambda calcul |
| Auteur(s): | Hamimed, Lyazid |
| Mots-clés: | Systèmes de preuve
Logique d'ordre supérieur
Déduction naturelle
Calcul des séquents
Paradoxe de curry |
| Date de publication: | 2006 |
| Résumé: | La majorité des systèmes de peuvre existantssont basés sur le paradigme " type as formula" due au typage du lambda calcul et plus précisément inspiré de l'interprétation de la relation des termes avec leurs types, Cette interprétation de la relation des termes avec leurs types, cette interprétation , connue souvent l'isomorphisme de Curry Howard, consiste à considérer les types comme étant des propositions et les termes comme étant des preuves le E-calcul est une extension du lambda calcul pur, ou une nouvelle procédure du processus de calcul est définie et deux constantes sont introduite: une de constantes est destinée à représenter l'implication et l'autre pour représenter la quantification universelle |
| Description: | 80 p. : ill. ; 30 cm |
| URI/URL: | http://dlibrary.univ-boumerdes.dz:8080/jspui/handle/123456789/914 |
| 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.
|
