Algèbre de Boole (structure)vignette|Exemple d'algèbre de Boole : l'ensemble des parties de l'ensemble {x, y, z} illustré par son diagramme de Hasse. En mathématiques, une algèbre de Boole, ou parfois anneau de Boole, est une structure algébrique étudiée en particulier en logique mathématique. Une algèbre de Boole peut être définie soit comme une structure ordonnée particulière, soit comme une structure algébrique particulière, soit comme un anneau (unitaire) dont tout élément égale son carré.
Switching circuit theorySwitching circuit theory is the mathematical study of the properties of networks of idealized switches. Such networks may be strictly combinational logic, in which their output state is only a function of the present state of their inputs; or may also contain sequential elements, where the present state depends on the present state and past states; in that sense, sequential circuits are said to include "memory" of past states. An important class of sequential circuits are state machines.
Anneau de BooleUn anneau de Boole (ou Algèbre de Boole), est un anneau unitaire (E, +, •, 0, 1) dans lequel tout élément a vérifie la relation a•a = a. Il découle immédiatement de la définition qu'un anneau de Boole est commutatif et que chaque élément est son propre opposé (en calculant le carré de x + 1, puis celui de x + y). En un sens qui peut être rendu précis, les anneaux de Boole sont les algèbres de Boole présentées autrement.
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).
SatisfaisabilitéEn logique mathématique, la satisfaisabilité ou satisfiabilité et la validité sont des concepts élémentaires de sémantique. Une formule est satisfaisable s'il est possible de trouver une interprétation (modèle), une façon d'interpréter tous les éléments constitutifs de la formule, qui rend la formule vraie. Une formule est universellement valide, ou en raccourci valide si, pour toutes les interprétations, la formule est vraie.
Problème SATvignette|Une instance du Sudoku peut être transformée en une formule de logique propositionnelle à satisfaire. Une assignation des variables propositionnelles donne une grille complétée. En informatique théorique, le problème SAT ou problème de satisfaisabilité booléenne est le problème de décision, qui, étant donné une formule de logique propositionnelle, détermine s'il existe une assignation des variables propositionnelles qui rend la formule vraie. Ce problème est important en théorie de la complexité.
Électronique numériqueL'électronique numérique concerne le système ou la technologie appliquée dont les caractéristiques sont exprimées par des valeurs de nombres, en anglais digital signifiant « chiffre ». La meilleure fiabilité lors de la transmission des signaux numérisés procure en principe, un contrôle de bout en bout de la chaîne des signaux. Le mode numérique permet de s'affranchir le plus souvent du bruit de fond, des parasites et autres artefacts lors de la transmission et améliore notamment le rapport signal sur bruit.
Assistant de preuveEn informatique (ou en mathématiques assistées par informatique), un assistant de preuve est un logiciel permettant la vérification de preuves mathématiques, soit sur des théorèmes au sens usuel des mathématiques, soit sur des assertions relatives à l'exécution de programmes informatiques. Beaucoup de projets ont été lancés pour formaliser les mathématiques, en 1966, Nicolaas de Bruijn lance le projet Automath, suivi par d'autres projets.
Isabelle (logiciel)The Isabelle automated theorem prover is a higher-order logic (HOL) theorem prover, written in Standard ML and Scala. As an LCF-style theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs without requiring yet supporting explicit proof objects. Isabelle is available inside a flexible system framework allowing for logically safe extensions, which comprise both theories as well as implementations for code-generation, documentation, and specific support for a variety of formal methods.
Problème 2-SATEn informatique théorique, le problème 2-SAT est un problème de décision. C'est une restriction du problème SAT qui peut être résolu en temps polynomial, alors que le problème général est NP complet. Le problème 2-SAT consiste à décider si une formule booléenne en forme normale conjonctive, dont toutes les clauses sont de taille 2, est satisfaisable. De telles formules sont appelées 2-CNF ou formules de Krom. On considère des formules en forme normale conjonctive, c'est-à-dire que ce sont des ET de OU de littéraux (un littéral est une variable ou la négation d'une variable).
Fonction booléennevignette|Arbre de décision binaire Une fonction booléenne est une fonction prenant en entrée une liste de bits et donnant en sortie un unique bit. Les fonctions booléennes sont très utilisées en informatique théorique, notamment en théorie de la complexité et en cryptologie (par exemple dans les boîtes-S et les chiffrements par flot -- fonction de filtrage ou de combinaison de registres à décalage à rétroaction linéaire). Une fonction booléenne est une fonction de dans où désigne le corps fini à 2 éléments.
Satisfiability modulo theoriesEn informatique et en logique mathématique, un problème de satisfiabilité modulo des théories (SMT) est un problème de décision pour des formules de logique du premier ordre avec égalité (sans quantificateurs), combinées à des théories dans lesquelles sont exprimées certains symboles de prédicat et/ou certaines fonctions. Des exemples de théories incluent la théorie des nombres réels, la théorie de l’arithmétique linéaire, des théories de diverses structures de données comme les listes, les tableaux ou les tableaux de bits, ainsi que des combinaisons de celles-ci.
