Horn-satisfiabilitéUne formule de Horn est une conjonction de clauses contenant chacune au plus un littéral positif, c'est-à-dire une conjonction de clauses de Horn. Puisque le problème SAT est NP-complet, donc vérifiable en temps polynomial et plus difficile que tout problème dans NP, il est naturel de rechercher des problèmes proches mais plus "faciles" à résoudre. C'est notamment le cas de la satisfaisabilité d'une formule de Horn, puisqu'il s'agit d'un problème P-complet, plus difficile que tout problème dans P.
Multiprotocol Label SwitchingDans les réseaux informatiques et les télécommunications, Multiprotocol Label Switching (MPLS) est un mécanisme de transport de données basé sur la commutation de labels (des « étiquettes »), qui sont insérés à l'entrée du réseau MPLS et retirés à sa sortie. À l'origine, cette insertion s'opère entre la couche de liaison de données (niveau 2) et la couche réseau (niveau 3) afin de transporter des protocoles comme IP. C'est pourquoi MPLS est qualifié de protocole de couche « 2,5 » ou « 2 / 3 ».
Complétude (logique)En logique mathématique et métalogique, un système formel est dit complet par rapport à une propriété particulière si chaque formule possédant cette propriété peut être prouvée par une démonstration formelle à l'aide de ce système, c'est-à-dire par l'un de ses théorèmes ; autrement, le système est dit incomplet. Le terme « complet » est également utilisé sans qualification, avec des significations différentes selon le contexte, la plupart du temps se référant à la propriété de la validité sémantique.
