Méthode formelle (informatique)En informatique, les méthodes formelles sont des techniques permettant de raisonner rigoureusement, à l'aide de logique mathématique, sur un programme informatique ou du matériel électronique numérique, afin de démontrer leur validité par rapport à une certaine spécification. Elles reposent sur les sémantiques des programmes, c'est-à-dire sur des descriptions mathématiques formelles du sens d'un programme donné par son code source (ou, parfois, son code objet).
Calcul des propositionsLe calcul des propositions ou calcul propositionnel, (ou encore logique des propositions) fait partie de la logique mathématique. Il a pour objet l'étude des relations logiques entre « propositions » et définit les lois formelles selon lesquelles les propositions complexes sont formées en assemblant des propositions simples au moyen des connecteurs logiques et celles-ci sont enchaînées pour produire des raisonnements valides. Il est un des systèmes formels, piliers de la logique mathématique dont il aide à la formulation des concepts.
Formule propositionnelleEn logique mathématique une proposition, ou formule propositionnelle, ou expression propositionnelle est une expression construite à partir de connecteurs et de variables propositionnelles. En logique propositionnelle classique, une formule propositionnelle, ou expression propositionnelle, est une formule bien formée qui possède une valeur de vérité. Si les valeurs de toutes les variables propositionnelles dans une formule propositionnelle sont données, une unique valeur de vérité peut être déterminée.
Méthode des tableauxvignette|200px|Représentation graphique d'un tableau propositionnel partiellement construit En théorie de la démonstration, les tableaux sémantiques sont une méthode de résolution du problème de la décision pour le calcul des propositions et les logiques apparentées, ainsi qu'une méthode de preuve pour la logique du premier ordre. La méthode des tableaux peut également déterminer la satisfiabilité des ensembles finis de formules de diverses logiques. C'est la méthode de preuve la plus populaire pour les logiques modales (Girle 2000).
Problème de l'arrêtvignette|L'animation illustre une machine impossible : il n'y a pas de machine qui lit n'importe quel code source d'un programme et dit si son exécution termine ou non. En théorie de la calculabilité, le problème de l'arrêt est le problème de décision qui détermine, à partir d'une description d'un programme informatique, et d'une entrée, si le programme s'arrête avec cette entrée ou non.
Synthèse de programmesEn informatique, la synthèse de programmes consiste à construire automatiquement un programme à partir d'une spécification. La spécification est décrite dans un langage logique, par exemple en logique temporelle linéaire. La synthèse de programmes s'appuie sur des techniques de vérification formelle de programmes. Le problème de synthèse de programmes remonte aux travaux d'Alonzo Church. Manna et Waldinger ont proposé une méthode déductive pour synthétiser un programme à partir d'une spécification en logique du premier ordre.
Canonical normal formIn Boolean algebra, any Boolean function can be expressed in the canonical disjunctive normal form (CDNF) or minterm canonical form, and its dual, the canonical conjunctive normal form (CCNF) or maxterm canonical form. Other canonical forms include the complete sum of prime implicants or Blake canonical form (and its dual), and the algebraic normal form (also called Zhegalkin or Reed–Muller). Minterms are called products because they are the logical AND of a set of variables, and maxterms are called sums because they are the logical OR of a set of variables.
Ressource (informatique)En informatique, les ressources sont des composants, matériels ou logiciels, connectés à un ordinateur. Tout composant de système interne est une ressource. Les ressources d'un système virtuel incluent les fichiers, les connexions au réseau, et les zones de mémoire. Selon le Grand dictionnaire terminologique, une ressource Internet est un élément d'intérêt pour un internaute et qui est disponible dans un des sites Internet du réseau.
Platine d'expérimentationUne platine d'expérimentation ou platine de prototypage (appelée en anglais breadboard, solderless breadboard, protoboard, plugboard ou encore Labdec du nom de la marque la plus répandue) est un dispositif qui permet de réaliser le prototype d'un circuit électronique et de le tester. L'avantage de ce système est d'être totalement réutilisable, car il ne nécessite pas de soudure. Ce dernier point distingue les platines d'expérimentation des veroboards, des perfboards ou des circuits imprimés qui sont, eux, utilisés pour réaliser des prototypes permanents et que l'on sera donc moins à même de démonter.
Effondrement (essai)Effondrement : Comment les sociétés décident de leur disparition ou de leur survie (Collapse: How Societies Choose to Fail or Survive) est un essai de l’écrivain américain Jared Diamond paru en 2005 et traduit en français en 2006. Il s’inscrit dans la lignée de son précédent ouvrage De l'inégalité parmi les sociétés paru en 1997 et traduit en français en 2000. Le sujet du livre est l’effondrement sociétal avec une composante environnementale, et dans certains cas également la contribution de changements climatiques, voisins hostiles, partenaires commerciaux, et également des problèmes de réponse sociétale.
