Réseau de neurones à propagation avantUn réseau de neurones à propagation avant, en anglais feedforward neural network, est un réseau de neurones artificiels acyclique, se distinguant ainsi des réseaux de neurones récurrents. Le plus connu est le perceptron multicouche qui est une extension du premier réseau de neurones artificiel, le perceptron inventé en 1957 par Frank Rosenblatt. vignette|Réseau de neurones à propagation avant Le réseau de neurones à propagation avant est le premier type de réseau neuronal artificiel conçu. C'est aussi le plus simple.
Démonstration (logique et mathématiques)vignette| : un des plus vieux fragments des Éléments d'Euclide qui montre une démonstration mathématique. En mathématiques et en logique, une démonstration est un ensemble structuré d'étapes correctes de raisonnement. Dans une démonstration, chaque étape est soit un axiome (un fait acquis), soit l'application d'une règle qui permet d'affirmer qu'une proposition, la conclusion, est une conséquence logique d'une ou plusieurs autres propositions, les prémisses de la règle.
Logique de HoareLa logique de Hoare, parfois appelée logique de Floyd-Hoare, est une méthode formelle définie par le chercheur en informatique britannique Tony Hoare dans un article de 1969 intitulé An Axiomatic Basis for Computer Programming. La méthode de Hoare met en place un formalisme logique permettant de raisonner sur la correction des programmes informatiques. Elle est fondée sur la syntaxe en ce sens que la correction d'un programme est décrite et démontrée par induction (récurrence) sur la structure du programme : à chaque règle syntaxique de construction d'un programme correspond une règle de la logique de Hoare.
Réseau de neurones artificielsUn réseau de neurones artificiels, ou réseau neuronal artificiel, est un système dont la conception est à l'origine schématiquement inspirée du fonctionnement des neurones biologiques, et qui par la suite s'est rapproché des méthodes statistiques. Les réseaux de neurones sont généralement optimisés par des méthodes d'apprentissage de type probabiliste, en particulier bayésien.
Couche transportthumb|Position de la couche transport dans le modèle ISO et dans TCP-IP En réseaux, la couche dite de transport constitue la quatrième couche du modèle OSI. Cette couche regroupe l'ensemble des protocoles chargés de la gestion des erreurs et du contrôle des flux réseaux. Les deux principaux protocoles utilisés sont les protocoles TCP et UDP. Modèle OSI La couche transport gère les communications de bout en bout entre processus. Cette couche est souvent la plus haute couche où on se préoccupe de la correction des erreurs.
Sémantique des langages de programmationEn informatique théorique, la sémantique formelle (des langages de programmation) est l’étude de la signification des programmes informatiques vus en tant qu’objets mathématiques. Comme en linguistique, la sémantique, appliquée aux langages de programmation, désigne le lien entre un signifiant, le programme, et un signifié, objet mathématique. L'objet mathématique dépend des propriétés à connaître du programme. La sémantique est également le lien entre : le langage signifiant : le langage de programmation le langage signifié : logique de Hoare, automates.
Runtime verificationRuntime verification is a computing system analysis and execution approach based on extracting information from a running system and using it to detect and possibly react to observed behaviors satisfying or violating certain properties. Some very particular properties, such as datarace and deadlock freedom, are typically desired to be satisfied by all systems and may be best implemented algorithmically. Other properties can be more conveniently captured as formal specifications.
Système axiomatiqueEn mathématiques, un système axiomatique est un ensemble d'axiomes dont certains ou tous les axiomes peuvent être utilisés logiquement pour dériver des théorèmes. Une théorie consiste en un système axiomatique et tous ses théorèmes dérivés. Un système axiomatique complet est un type particulier de système formel. Une théorie formelle signifie généralement un système axiomatique, par exemple formulé dans la théorie des modèles. Une démonstration formelle est une interprétation complète d'une démonstration mathématique dans un système formel.
Preuve de travailUn système de validation par preuve de travail (en anglais : proof of work, PoW) est, en informatique, un protocole permettant de repousser, sur un environnement client-serveur, des attaques par déni de service ou d'autres abus de service tels que les spams. Ce système de preuve de travail est utilisé dans des cadres beaucoup plus complexes, pour la validation des transactions de la blockchain de certaines crypto-monnaies comme le Bitcoin. Cette vérification par les mineurs de bitcoins est récompensée par l'émission de nouveaux bitcoins au bénéfice des vérificateurs.
Lean (assistant de preuve)Lean est un assistant de preuve et un langage de programmation. Il repose sur le principe de calcul des constructions avec types inductifs. Lean possède un certain nombre de fonctionnalités notables qui le distinguent des autres logiciels d'assistance à la preuve. Lean peut être compilé vers du JavaScript, et est ainsi accessible dans un navigateur Web. Il prend en charge nativement les caractères Unicode des symboles mathématiques, qui peuvent être saisis grâce à des raccourcis rappelant la syntaxe de LaTeX (par exemple, "×" s'obtient en tapant "\times").
