Connecteur logiqueEn logique, un connecteur logique est un opérateur booléen utilisé dans le calcul des propositions. Comme dans toute approche logique, il faut distinguer un aspect syntaxique et un aspect sémantique. D'un point de vue syntaxique, les connecteurs sont des opérateurs dans un langage formel pour lesquels un certain nombre de règles définissent leur usage, au besoin complétées par une sémantique. Si l'on se place dans la logique classique, l'interprétation des variables se fait dans les booléens ou dans une extension multivalente de ceux-ci.
Logique polyvalenteLes logiques polyvalentes (ou multivalentes, ou multivaluées) sont des alternatives à la logique classique aristotélicienne, bivalente, dans laquelle toute proposition doit être soit vraie soit fausse. Elles sont apparues à partir des années 1920, surtout à la suite des travaux du logicien polonais Jan Łukasiewicz. Elles sont principalement étudiées au niveau du seul calcul propositionnel et peu au niveau du calcul des prédicats.
Logique mathématiqueLa logique mathématique ou métamathématique est une discipline des mathématiques introduite à la fin du , qui s'est donné comme objet l'étude des mathématiques en tant que langage. Les objets fondamentaux de la logique mathématique sont les formules représentant les énoncés mathématiques, les dérivations ou démonstrations formelles représentant les raisonnements mathématiques et les sémantiques ou modèles ou interprétations dans des structures qui donnent un « sens » mathématique générique aux formules (et parfois même aux démonstrations) comme certains invariants : par exemple l'interprétation des formules du calcul des prédicats permet de leur affecter une valeur de vérité'.
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.
Couple (mathématiques)En mathématiques, un couple de deux objets est la donnée de ces deux objets dans un ordre déterminé. Le couple des deux objets et est noté . Si et sont distincts, le couple est distinct du couple ; en cela, la notion de couple se distingue de la notion de paire où l'ordre des éléments est indifférent. Pour désigner un couple, les anglophones emploient d'ailleurs ordered pair, c’est-à-dire paire ordonnée. Les objets a et b sont appelés respectivement première composante et deuxième composante du couple (a, b).
Contrainte (mathématiques)En mathématiques, une contrainte est une condition que doit satisfaire la solution d'un problème d'optimisation. On distingue deux types de contraintes : les contraintes d'égalité et les contraintes en inégalité. L'ensemble des solutions satisfaisant toutes les contraintes est appelé l'ensemble admissible. On considère un problème d'optimisation classique : avec et et désigne le vecteur . Dans cet exemple, la première ligne montre la fonction à minimiser (appelée fonction objectif ou fonction-coût) mais aussi l'ensemble où la solution doit être recherché, ici C.
Arithmétique de PresburgerEn logique mathématique, l'arithmétique de Presburger est la théorie du premier ordre des nombres entiers naturels munis de l'addition. Elle a été introduite en 1929 par Mojżesz Presburger. Il s'agit de l'arithmétique de Peano sans la multiplication, c’est-à-dire avec seulement l'addition, en plus du zéro et de l'opération successeur. Contrairement à l'arithmétique de Peano, l'arithmétique de Presburger est décidable. Cela signifie qu'il existe un algorithme qui détermine si un énoncé du langage de l'arithmétique de Presburger est démontrable à partir des axiomes de l'arithmétique de Presburger.
Calcul des prédicatsEn logique mathématique, le calcul des prédicats du premier ordre, ou calcul des relations, logique quantificationnelle, ou tout simplement calcul des prédicats, est un système formel utilisé pour raisonner et décrire des énoncés en mathématiques, informatique, intelligence artificielle, philosophie et linguistique. Il a été proposé par Gottlob Frege une formalisation du langage des mathématiques entre la fin du et le début du .
Ordre totalEn mathématiques, on appelle relation d'ordre total sur un ensemble E toute relation d'ordre ≤ pour laquelle deux éléments de E sont toujours comparables, c'est-à-dire que On dit alors que E est totalement ordonné par ≤. Une relation binaire ≤ sur un ensemble E est un ordre total si (pour tous éléments x, y et z de E) : x ≤ x (réflexivité) ; si x ≤ y et y ≤ x, alors x = y (antisymétrie) ; si x ≤ y et y ≤ z, alors x ≤ z (transitivité) ; x ≤ y ou y ≤ x (totalité). Les trois premières propriétés sont celles faisant de ≤ une relation d'ordre.
Structure de donnéesEn informatique, une structure de données est une manière d'organiser les données pour les traiter plus facilement. Une structure de données est une mise en œuvre concrète d'un type abstrait. Pour prendre un exemple de la vie quotidienne, on peut présenter des numéros de téléphone par département, par nom, par profession (comme les Pages jaunes), par numéro téléphonique (comme les annuaires destinés au télémarketing), par rue et/ou une combinaison quelconque de ces classements.
