Note publique d'information : DANS CE MEMOIRE EST ETUDIE UN CAS REEL DE FORMALISATION. LE PROBLEME DE LA FORMALISATION
EST EXPLORE EN CHERCHANT UNE FACON D'AUTOMATISER LES SOLUTIONS DE CE CAS REEL, DANS
LE CADRE D'UNE APPROCHE DE LA RESOLUTION DISTRIBUEE DU PROBLEME. DANS LE CADRE DE
LA FORMALISATION DU PROBLEME, SONT DEFINIS DES SYSTEMES LOGIQUES CAPABLES DE FOURNIR
UN LANGAGE DE REPRESENTATION DE CONNAISSANCES EN MEME TEMPS UNE MANIERE D'AUTOMATISER
LES DEDUCTIONS POUR CE CAS REEL. SONT FINALEMENT PROPOSEES DES SOLUTIONS CONCRETES,
AU NIVEAU INFORMATIQUE, POUR LE PROBLEME ETUDIE. LE CAS REEL UTILISE POUR REALISER
CES OBJECTIFS A ETE LE PROBLEME DE LA COLLISION ENTRE AVIONS, LE PROJET SALOME. NOUS
AVONS CONSTATE LE BESOIN DE LA DEFINITION D'UN NOUVEAU DOMAINE, APPELE GENIE LOGIQUE:
UNE TECHNIQUE BASEE SUR DES PRINCIPES LOGIQUES DANS LE BUT D'UNE APPLICATION DE CES
PRINCIPES AUX PROBLEMES REELS. DANS LE CADRE DE LA FORMALISATION DES PROBLEMES REELS
EST ETUDIE LE CAS SALOME. PAR RAPPORT AUX BESOINS DE CE CAS, UNE LOGIQUE MULTI-MODALE
PROPOSITIONNELLE DONT LE LANGAGE PEUT EXPRIMER DES CONNAISSANCES EPISTEMIQUES, DOXASTIQUES
ET TEMPORELLES, APPELE KB, EST DEFINIE. DE MEME, A ETE ETUDIE LE PROBLEME DU TRAITEMENT
FORMEL DES CONTRADICTIONS. AINSI, UNE NOUVELLE SEMANTIQUE POUR LA PARACONSISTANCE
A ETE DEFINIE ET UNE LOGIQUE PROPOSITIONNELLE POUR UNE SOCIETE A DEUX AGENTS, SL#2,
ET UNE LOGIQUE PROPOSITIONNELLE POUR UNE SOCIETE HOMOGENE A PLUSIEURS AGENTS, SL#C,
ONT ETE OBTENUES. FINALEMENT, SL#C ET KB ONT ETE MELANGEES. AINSI, S5KB EST CONSTRUITE,
UNE LOGIQUE PROPOSITIONNELLE MULTI-MODALE CAPABLE DE MANIPULER DES CONNAISSANCES EPISTEMIQUES,
DOXASTIQUES, TEMPORELLES ET CONTRADICTOIRES. FINALEMENT, UN DEMONSTRATEUR AUTOMATIQUE
DE THEOREME POUR DES LOGIQUES NON CLASSIQUES, TIM, A PERMIS D'IMPLEMENTER LES LOGIQUES
KB ET S5KB. L'ASSOCIATION DES FORMALISMES, CREES POUR CE PROJET, AVEC DES PRINCIPES
SITUES DANS L'AXE DE LA RESOLUTION DISTRIBUE DE PROBLEME, A PERMIS DE DEMONTRER LA
FAISABILITE D'UN SYSTEME ANTICOLLISION D'AVIONS