Abstract FR:

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