Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Théorie des modèles finis
Résumé
La théorie des modèles finis est un sous-domaine de la théorie des modèles. Cette dernière est une branche de la logique mathématique qui traite de la relation entre un langage formel (la syntaxe) et ses interprétations (ses sémantiques). La théorie des modèles finis est la restriction de la théorie des modèles aux interprétations de structures finies, donc qui sont définies sur un ensemble (un univers) fini. Ses applications principales sont la théorie des bases de données, la complexité descriptive et la théorie des langages formels.
La théorie des modèles est proche de l'algèbre. En informatique, la théorie des modèles finis est devenue un instrument « unusually effective ». En d'autres termes, et pour citer Immerman : . Les applications principales de la théorie des modèles finis sont : la complexité descriptive, la théorie des bases de données et la théorie des langages formels.
De nombreux théorèmes de la théorie des modèles cessent d'être vrais si on les restreint aux structures finies. Il en résulte que la théorie des modèles finis n'a plus les mêmes méthodes de démonstration. Parmi les résultats centraux de la théorie des modèles classique qui sont faux pour les structures finies, il y a le théorème de compacité, le théorème de complétude de Gödel et la méthode des ultraproduits pour la logique du premier ordre. Il est donc utile de disposer d'outils spécifiques, dont le premier est le jeu d'Ehrenfeucht-Fraïssé.
La théorie des modèles traite de définissabilité de structures. La motivation usuelle est la question de savoir si une classe de structures peut être décrite, à un isomorphisme près, dans un langage logique donné : par exemple, est-il possible de définir les graphes cycliques par une formule, de logique du premier ordre par exemple, en trouvant une formule qui est vérifiée par ces graphes seulement ? Ou, autrement dit, est-ce que la propriété « être cyclique » est définissable en logique du premier ordre ?
Une structure isolée peut toujours être décrite de manière unique en logique du premier ordre.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.