paprika.idref.fr paprika.idref.fr data.idref.fr data.idref.fr Documentation Documentation
Identifiant IdRef : 211322555Copier cet identifiant (PPN)
Notice de type Rameau

Point d'accès autorisé

Informations

Langue d'expression : Francais
Date de naissance :  1999
Note publique d''information : 
LA NOTION DE PREUVES EN PROGRAMMATION LOGIQUE EST EXAMINEE A DEUX NIVEAUX DIFFERENTS. D'UN POINT DE VUE EXTERNE, LA THEORIE CLASSIQUE DE LA PROGRAMMATION LOGIQUE EST COMPLETEMENT FORMALISEE DANS LE CALCUL DES CONSTRUCTIONS INDUCTIVES. APRES AVOIR ENVISAGE LE PROBLEME DE LA DEFINITION DE FONCTIONS PARTIELLES DANS UN SYSTEME DANS LEQUEL SEULES LES FONCTIONS TOTALES SONT REPRESENTABLES, L'UNIFICATION EST OBTENUE EN REUTILISANT UNE PREUVE FORMELLE EXISTANTE PORTANT SUR UN SUR-ENSEMBLE DES TERMES. LES PROPRIETES FONDAMENTALES DE LA SLD-RESOLUTION SONT ALORS FORMALISEES. LE NIVEAU DE DETAIL IMPOSE PAR LA MECANISATION DES PREUVES CONSIDEREES A MIS EN RELIEF LA COMPLEXITE CACHEE DE CERTAINES PREUVES : LE MECANISME DE RENOMMAGE EST TRAITE DE MANIERE EXPLICITE, TRANSFORMANT AINSI CERTAINES CERTITUDES THEORIQUES EN REALITES. D'UN POINT DE VUE INTERNE, LES PREUVES SLD, FINIES OU INFINIES, SONT COMPAREES A CELLES QUE L'ON PEUT OBTENIR, PAR INDUCTION OU PAR CO-INDUCTION, A PARTIR DES CLAUSES D'UN PROGRAMME LOGIQUE VUES COMME DES REGLES D'INFERENCE. DANS LE CAS FINI LA CORRESPONDANCE EST COMPLETE (CE QUE CALCULE UN PROGRAMME EST PROUVABLE) TANDIS QUE DANS LE CAS INFINI, CERTAINS OBJETS NON CALCULABLES SONT TOUTEFOIS PROUVABLES. LES PROPRIETES CLASSIQUES DES DEFINITIONS CO-INDUCTIVES ET LA COMPARAISON DE CERTAINES DERIVATIONS INFINIES A DES TERMES DE PREUVE D'UN TYPE CO-INDUCTIF, SE REVELENT UTILES TANT POUR EXPLIQUER LES RESULTATS D'INCOMPLETUDE D'APPROCHES EXISTANTES QUE POUR DEFINIR UNE SEMANTIQUE VALIDE ET COMPLETE POUR UNE CLASSE DE DERIVATION INFINIES (PRECISEMENT CELLES QUI NE CONSTRUISENT PAS DE TERMES INFINIS).

Notices d'autorité liées

Autres identifiants

Utilisation dans Rameau

Le point d'accès peut être employé dans un point d'accès sujet

Equivalent dans un autre référentiel

... Références liées : ...