Date : 2001
Editeur / Publisher : [S.l.] : [s.n.] , 2001
Format : 147 p.
Type : Livre / Book
Type : Thèse / ThesisLangue / Language : français / French
Relation : THEORIE DES TYPES ET RECRITURE / FREDERIC BLANQUI / Villeurbanne : [CCSD] , 2006
Résumé / Abstract : CETTE THESE TRAITE DE LOGIQUE ET DE CALCUL. UNE DEMONSTRATION MATHEMATIQUE EST GENERALEMENT CONSTITUEE DE RAISONNEMENTS ET DE CALCULS. OR IL S'AVERE QUE LA PLUPART DES SYSTEMES DE DEVELOPPEMENT DE PREUVES ACTUELS NEGLIGENT L'ASPECT CALCUL, CE QUI LES REND DIFFICILES A UTILISER PAR DES NON-SPECIALISTES. PAR AILLEURS, CES SYSTEMES, COMME LE CALCUL DES CONSTRUCTIONS INDUCTIVES, PERMETTENT D'EXPRIMER DE TRES NOMBREUSES FONCTIONS (TOUTE FONCTION DONT L'EXISTENCE EST PROUVABLE EN ARITHMETIQUE INTUITIONNISTE D'ORDRE SUPERIEUR), MAIS CES DEFINITIONS PEUVENT ETRE MALAISEES ET PARFOIS INEFFICACES. LES DEFINITIONS A L'AIDE DE REGLES DE RECRITURE SONT A LA FOIS PLUS GENERALES, PLUS AISEES ET PEUVENT ETRE PLUS EFFICACES. C'EST POURQUOI NOUS PROPOSONS D'ETENDRE LE CALCUL DES CONSTRUCTIONS PAR DES SIGNATURES ET DES REGLES DE RECRITURE INTRODUITES PAR L'UTILISATEUR. NOUS ETUDIONS LES PROPRIETES D'UN TEL CALCUL ET, POUR ASSURER LA COHERENCE LOGIQUE DU FORMALISME ET LA DECIDABILITE DU TYPAGE, NOUS FOURNISSONS DES CONDITIONS SUR LES REGLES DE RECRITURE DONNEES PAR L'UTILISATEUR. UNE TELLE EXTENSION N'EST PAS NOUVELLE MAIS NOS CONDITIONS GENERALISENT CELLES PROPOSEES JUSQU'A MAINTENANT. EN PARTICULIER, NOUS AUTORISONS DES REGLES DE RECRITURE AU NIVEAU DES PREDICATS, CE QUI PERMET LA FORMALISATION, A L'INTERIEUR DU SYSTEME, DE PROCEDURES DE DECISION POUR LA DEMONSTRATION AUTOMATIQUE.