Mots-clés:
  - Démonstration automatique
  - Théorie des types
  - Raisonnement automatique

Equipes
  Toccata

Equipes-projets Inria communes


Resultats majeurs
  DL-liteR in the Light of Propositional Logic for Decentralized Data Management
  Non-conservative Extension of a Peer in a P2P Inference System
  Robust Module-based Data Management
  Query Containment in Description Logics Reconsidered
  On the Complexity of Consistent Query Answering in the Presence of Simple Ontologies

Contrats
  CAT
  GT CMF
  UNLOC

Logiciels et brevets


Collaborations


Membres
  DE ROUGEMONT Michel
  GOASDOUE François
  COLAZZO Dario
  STOULS Nicolas
  BARDOU Romain
  LASSAIGNE Richard
  BOURGNE Gauvain

Thèses et habilitations
  Preuves mécanisées de propriétés de programmes
  Propagation et affinement d'hypothèses sous contraintes communicationnelles

° Algorithmes pour les grands volumes de données distribuées
° Algorithmique des systèmes en réseau
° Algorithmique distribuée
° Architectures parallèles
° biologie de synthese
° Biologie des systèmes
° Biologie structurale
° biologie synthetique
° Calcul à haute performance
° Calcul quantique
° Calibration d'algorithmes (sélection, ajustement d'hyper-paramètres)
° Codage réseau
° Collaboration médiatisée
° Combinatoire
° Compilation et optimisation des programmes
° Décision optimale en contexte incertain
° Définition de nouveaux critères
° Démonstration automatique, SMT et applications
° Distributed Design
° Fab lab
° Fabrication Numérique
° Formalisation de langages (de spécification et de programmation) dans les assistants de preuve
° Formalisation et preuves de programmes numériques
° Gestion de données du Web
° Ingénierie des systèmes interactifs