ACL2 (A Computational Logic for Applicative Common Lisp) permet de démonter les théorèmes pour des applications industrielles. C'est à la fois de la logique mathématique et un système d'outils pour construire des preuves dans la logique. ACL2 marche avec GCL (GNU Common Lisp).

L'IA Kernel est un moteur d'intelligence artificielle réutilisable qui utilise le traitement du langage naturel et un modèle Activateur/Contexte afin de permettre le multi-tâche entre les cellules installées.

En gros, cette bibliothèque offre au programmeur une série d'algorithmes de recherche qui peuvent êtres utilisés pour résoudre toutes sortes de problèmes différents. L'idée est que lorsqu'il développe un logiciel de résolution de problème, le programmeur devrait pouvoir se concentrer sur la représentation du problème à résoudre, sans avoir à se soucier de l'implémentation du moteur de recherche qui serait précisément utilisé pour mener la recherche. Cette idée a été appliquée grâce à l'implémentation d'une série de classes de recherche qui peuvent être incorporées dans d'autres logiciels à travers des spécifications de dérivation ou d'héritage du C++. Les algorithmes de recherche suivants ont été mis en oeuvre :

Il existe un livre qui correspond à cette bibliothèque, "Object-Oriented Artificial Instelligence, Using C++"

Ce document fournit des informations de référence sur "A Learning Engine for Proposing Hypotheses" (Aleph : un moteur d'apprentissage pour proposer des hypothèses). Aleph est système de programmation par logique inductive (Inductive Logic Programming, ILP). La fonction d'Aleph est celle de prototype pour explorer des idées. Aleph est un algorithme ILP mis en oeuvre en Prolog par le Dr Ashwin Srinivasav au laboratoire informatique de l'université d'Oxford, et a été écrit scpécifiquement pour la compilation avec le compilateur Prolog YAP.

La fondation CIL (les échecs en Lisp) est une implémentation "Common Lisp" de toutes les fonctions principales nécessaires au développement d'applications sur les jeux d'échecs. Le but principal du projet CIL est d'amener les chercheurs en IA intéressés par l'emploi de Lisp à travailler sur le domaine des échecs.

C'est une bibliothèque pour le langage de programmation Python qui fournit une interface orientée objet à l'outil système expert CLIPS. Il inclut une interface pour COOL (CLIPS Object Oriented Langage : Langage orienté objet CLIPS) qui permet de :

La bibliothèque gratuite de logique floue (FFLL : Free Fuzzy Logic Library) est une bibliothèque de classe et une API libres de logique floue qui est optimisée pour des applications dont la rapidité est importante, comme les jeux vidéos. FFLL est capable de charger des fichiers conformes au standard IEC 61131-7.

La boîte à outils du modèle de Markov masqué (HTK : Hidden Markov Model ToolKit) est une boîte à outils portable pour créer et manipuler des modèles de Markov masqué. HTK consiste en une série de modules de bibliothèques et d'outils disponibles sous la forme de sources en C. Ces outils founissent des solutions sophistiquées pour l'analyse vocale, la formation HMM, les tests et l'analyse de résultats. L'application supporte les HMM en utilisant à la fois les fonctions gaussiennes sur les mélanges à densité constante et les distributions discrètes et peut être utilisée pour créer des systèmes HMM complexes. Le logiciel HTK contient une grande quantité d'informations et d'exemples.

JACK est une nouvelle bibliothèque fournissant programmation et recherche des contraintes pour Java.

Les sources et la documentation sont disponibles au lien ci-dessus.

LK est une implémentation de l'heuristique de Lin-Kernighan pour le problème du voyageur de commerce et pour le problème de la correspondance parfaite de pondération minimum. Il est spécialement adapté aux figures géométriques en 2D, et a été appliqué dans certains exemples jusqu'à un million de villes. Il comprend aussi des générateurs d'exemples et des scripts Perl pour manipuler les exemples TSPLIB

Cette implémentation introduit la "compensation groupée efficace", une technique algorithmique expérimentale dont le but est de rendre l'heuristique de Lin-Kernighan plus robuste dans le cas de données groupées.

Le projet de musique informatisée (Computer Music Project) au CMU développe la technologie de la musique informatisée, et de la performance interactive pour améliorer l'expérience et la créativité musicale de l'homme. Cet effort interdisciplinaire puise dans la théorie de la musique, dans les sciences cognitives, l'intelligence artificielle, l'apprentissage des machines, l'interaction homme-machine, les systèmes temps réelles, les graphismes et animations informatiques, le multimédia, les langages de programmation, le traitement du signal. Un exemple paradigmatique de ces efforts interdisciplinaires est la création de la performance interactive qui lie l'improvisation musicale de l'homme aux agents informatiques intelligents en temps réel.

OpenCyc est la version libre de Cyc, la plus grande et la plus complète des bases de connaissance générale ainsi que le plus grand moteur de raisonnement de sens communs. Cette connaissance des choses est basée sur 6000 concepts en relation avec 6000 affirmations.

La banque de connaissances sur le domaine publique (PDKB : Public Domain Knowledge Bank) est une banque de connaissances sur l'intelligence artificielle des loi et faits de sens commun. Elle est basée sur l'ontologie de niveau supérieur de Cyc (CUO : Cyc Upper Ontology) et le langage MFLD.

C'est un simple module python pour la logique floue. Le fichier est 'fuz.tar.gz' dans ce répertoire. L'auteur ambitionne également d'écrire un algorithme de génétique simple de même qu'une bibliothèque sur les réseaux neuronaux. Regarder le fichier '00_index' dans ce répertoire pour obtenir des informations sur la version.

Quant/1 signifie QUANTifieur de type 1. Son but est d'être une alternative pour les systèmes semblables à Prolog (ou résolutionnaux). Les principales caractéristiques comprennent la non-nécéssité d'éliminer les quantifieurs, la scolémisation, la facilité de compréhension, les opérations sur des formules de grande échelle, l'acceptation de fomules 'nonHorn', l'approfondissement iterratif. La bibliothèque réelle implémentée dans ce projet est appelée ATPPCF (Automatic Theorem Prover in calculus of Positively Constructed Formulae : preuve automatique du théoreme dans le calcul de formules construites positivement)

ATPPCF deviendra une bibliothèque (moteur inférant) et une extension du langage de calculs de prédiction comme un nouveau langage logique. Cette bibliothèque sera incorporable dans d'autres programmes, comme TCL, Python, Perl. La méthode d'inférance primaire du moteur sera la "recherche d'inférances dans le langage des formules construites positivement (PCF : Positively Constructed Formulas)" (comme un sous-ensemble de calculs de prédicats bien traduits dans les deux sens). Le langage sera utilisé comme langage de script pour le moteur. Mais il y aura la possibilité de le remplacer par des extension de langage du programme principal.

Screamer est une extension de Common Lisp qui ajoute un support pour la programmation non déterministe. Screamer comprend deux niveaux. Le niveau non déterministe basique ajoute un support pour la journalisation et les effets de coté irréalisables. En plus de cet aspect non deterministe, Screamer fournit un langage complet de programmation sous contraintes dans lequel on peut formuler et résoudre un mélange de systèmes sous contraintes numériques ou symboliques. Ensembles, ces deux niveaux étendent Common Lisp avec pratiquement toutes les fonctionnalités de Prolog et des languages de programmation logiques sous contraintes comme CHiP ou CLP(R). En outre, Screamer est complètement compatible avec Common Lisp. Les programmes de Screamer peuvent coexister et interopérer avec d'autres extensions de Common Lisp comme CLOS, CLIM et Iterate.

SPASS : Démontreur de théorèmes automatisé pour des logiques de 1er ordre avec égalité.

Si vous êtes intéressés par les démonstrations de théorèmes de logique du premier ordre, l'analyse formelle de programmes, systèmes, protocoles, les approches formelles de projets sur l'IA, les procédures de décisions, la démonstration de théorèmes à logique modale, SPASS peut vous offrir de bonnes fonctionnalités.

ThoughtTreasure est un projet pour créer une base de données de règles de sens communs à utiliser dans n'importe quelle application. Il consiste en une base de donnnées d'un peu plus de 100 000 règles et d'une API C pour l'intégrer dans vous applications. Les emballeurs Python, Perl, Java et TCL sont déjà disponibles.

Torch est une bibliothèque d'apprentissage écrit en C++. Son but est de fournir la crème des meilleurs algorithmes. Il est, et sera, en développement incessant.

Torch est une bibliothèque libre dont les auteurs encouragent tout le monde à développer de nouveaux logiciels qui seront inclus dans les versions futures du site officiel.

ASA (Adaptive Simulated Annealing : Recuit simulé adaptatif) est un puissant algorithme en code C d'optimisation globale particulièrement pratique pour les systèmes non linéaires et/ou stochastiques.

ASA est développé pour trouver statistiquement le meilleur ajustement global d'une fonction coût non linéaire et non convexe sur un espace de dimension D. Cet algorithme permet un schéma de refroidissement du recuit pour une température T exponentiellement décroissante dans le temps recuit k, T=T_0 exp(-c k^1/D). L'introduction du renouvellement de recuit permet également une adaptation aux changements de sensibilités dans un espace paramétrique multi-dimensionnel. Cet schéma de refroidissement de recuit est plus rapide que le recuit de Cauchy rapide, où T = T_0/k, et encore plus rapide que le recuit de Boltzmann, où T = T_0/ln k.

BABYLON est un environnement modulaire, configurable et hybride pour le développement de systèmes experts. Ses caractéristiques comprennent des objets et règles avec un chaînage vers l'avant et vers l'arrière, une logique Prolog et des contraintes. BABYLON est codé et incorporé en Common Lisp.

Cfengine, ou "moteur de configuration" est un langage de très haut niveau pour la construction de systèmes experts qui administrent et configurent de grands réseaus informatiques. Cfengine utilise l'idée de classes et une primitive formée d'intelligence pour définir et automatiser la configuration de grands systèmes de façon la plus économique possible. Cfengine est conçu pour être une part des système immunisés informatiques.

Le système CLEAR est un environnement graphique interactif pour les sémantiques de calcul. L'outil permet l'exploration et la comparaison de différents formalismes sémantiques ainsi que de leur interaction avec la syntaxe. Cela permet à l'utilisateur d'obtenir une idée de l'étendue des possibilités en matière de construction sémantique, ainsi qu'où se trouve la convergence réelle entre les théories.

CLIG est un grapheur interactif et renouvelable pour visualiser les structures de données linguistiques comme les arbres, les structures des caractéristiques, les Structures de Représentation de Discours (DRS), formules logiques, etc. Chacun de ces éléments peut être mélangé librement et incorporé aux autres. Le grapher a été conçu à la fois pour marcher tout seul et pour être utilisé comme une extension pour les applications linguistiques qui affichent leur résultat d'une manière graphique.

CLIPS est un outil productif de système expert de développement et de livraison qui fournit un environnement complet pour la construction de systèmes experts basés sur des règles et/ou des objets.

CLIPS fournit un outil cohésif pour la gestion d'une grande variété de connaissances compatible avec trois différents paradigmes de programmation : basé règles, orienté objet et procédural. La programmation basée règle permet de représenter les connaissances comme de l'heuristique, ou des "règles empiriques", qui spécifient une série d'actions à entreprendre pour une situation donnée. La programmation orientée objet permet à des sytèmes complexes d'être modelés comme composants modulaires (qui peuvent être facilement réutilisés pour modeler d'autres systèmes ou pour créer de nouveaux composants). Les capacités de programmation procédurale fournies par CLIPS sont similaires à celles trouvées dans les langages comme le C, le Pascal, l'Ada et le Lisp.

EMA-XPS est un interpréteur de commande [shell] de système expert graphique hybride basé sur le shell orienté ASCII Babylon 2.3 du Centre National Allemand de Recherche pour les Sciences Informatiques (GMD). En plus de la puissance IA de Babylon (représentation de données orientées objet, règles de chaînage vers l'avant et vers l'arrière - regroupables en séries, en clauses de Horn, et en réseaux contraints), une interface graphique basée sur le système X11 Window System et la OSF/Motif Widget Library ont été fournies.

FOOL signifie organisateur flou Oldenburg [Fuzzy Organizer OLdenburg]. C'est le résultat d'un projet de l'Université d'Oldenburg. FOOL est une interface utilisateur graphique pour développer les règles de base floues. FOOL va vous aider à inventer et maintenir une base de donnée qui spécifie le comportement d'un contrôleur flou ou semblable.

FUF est une implémentation étendue du formalisme des grammaires d'unification fonctionnelles (FUGs : functional unification grammars) introduit par Martin Kay, spécialisé dans la tâche de génération du langage naturel. Il ajoute les fonctionnalités suivantes au formalisme de base :

Ces extensions permettent le développement de grandes grammaires qui peuvent être traitées efficacement et peuvent être maintenues à jour et comprises plus facilement. SURGE est une grande grammaire syntaxique de réalisations de l'anglais, écrite en FUF. SURGE est développé pour servir de composant de génération syntaxique de boîte noire dans un système de génération plus grande qui encapsule une connaissance riche de la syntaxe anglaise. SURGE peut aussi être utilisé comme plate-forme pour l'exploration de l'écriture de la grammaire dans une perspective de génération.

Semble être obsolète ??? N'est plus sur le site, bien que le projet parent se poursuit toujours.

The Grammar Workbench (L'atelier de grammaire), ou GWB en abrégé, est un environnement pour le développement aisé de grammaires Affix dans le formalisme AGFL. Ses buts sont :

The GSM Suite (la suite GSM) est une série de programmes pour l'utilisation des machines à état fini à la mode graphique. Cette "suite" consiste en des programmes qui éditent, compilent, et impriment des machines d'état. Cette "suite" comprend un programme d'édition, gsmedit, un compilateur, gsm2cc, qui produit une implémentation C++ d'une machine d'état, un générateur PostScript, gsm2ps, et deux autres programmes mineurs. GSM possède la licence publique GNU et est donc libre pour l'utilisation selon les termes de cette licence.

Illuminator est une panoplie d'outils pour développer des applications OCR et de Compréhension d'Image. Illuminator possède deux parties majeures : une bibliothèque pour représenter, stocker et récupérer les information OCR, entrée en vigueur sous le nom "daflibs", et un lecteur X-Windows de fichiers "DAFS", appelé "illum". Illuminator et DAFSlib ont été conçus pour supplanter les formats OCR existants et pour devenir un standard dans l'industrie. Ils sont particulièrement extensibles pour manipuler d'avantage que juste l'anglais.

Caractéristiques de cette version :

Isabelle est un démontreur de théorème générique populaire développé à l'Université de Cambridge et au TU Munich. Les logiques existantes comme Isabelle/HOL fournissent un environnement de démontreur de théorème prêt à être utilisé pour des applications de taille. Isabelle peut également servir comme châssis pour un prototypage rapide de systèmes déductifs. Il est présenté avec une grande bibliothèque comprenant Isabelle/HOL (logique classique d'ordre supérieur), Isabelle/HOLFS (Logique de Scott pour des fonctions calculatoire avec HOL), Isabelle/FOL (logique du premier ordre classique et intuitive), et Isabelle/ZF (ensemble de théories de Zermelo-Fraenkel au dessus de FOL).

Jess (le shell système expert Java) est un clone du populaire shell système expert CLIPS écrit entièrement en Java. Avec Jess, vous pouvez à votre convenance donner à vos applets l'habilité à raisonner. Jess est compatible avec toutes les versions de Java, à partir de la version 1.0.2. Jess implémentes les constructeurs suivants de CLIPS : defrules, deffunctions, defglobals, deffacts, et deftemplates.

Learn (apprendre) est programme d'apprentissage vocal avec un modèle de mémoire.

LISA (Lisp-based Intelligent Software Agents : agents logiciels intelligents basé sur Lisp) est un système de règles de production lourdement influencé par JESS (Java Expert System Shell). Il a en son squelette un moteur de raisonnement basé sur l'algorithme de filtrage de Rete. LISA fournit également l'habilité à raisonner sur les objets CLOS ordinaires.

NICOLE (Nearly Intelligent Computer Operated Language Examiner) est une théorie ou une expérimentation qui, si on donne à un ordinateur suffisamment de combinaisons de liaisons entre comment des mots, groupes de mots ou phrases, peut vous répondre. C'est un essai pour simuler une conversation en apprenant comment les mots se rapportent à d'autres mots. Un humain communique avec NICOLE via le clavier et NICOLE répond avec ses propres phrases qui sont automatiquement générées, basées sur ce que NICOLE a stocké dans sa base de données. Chaque nouvelle phrase qui a été écrite et que NICOLE ne connaît pas est ajoutée à la base de donnée de NICOLE, ce qui étend la base de connaissances de NICOLE.

Notre système de déduction automatisé courant Otter est conçu pour démontrer les théorèmes statiques de logique du premier ordre avec une égalité. Les règles d'inférence d'Otter sont basées sur la résolution et la paramodulation, et il comprend des procédures pour la réécriture de termes, l'ordonnancement de termes, la complétion Knut-Bendix, le pesage, et les stratégies pour diriger et restreindre les recherches de preuves. Otter peut aussi être utilisé comme un calculateur symbolique et a un système de programmation équationnelle incorporé.

PVS est un système de vérification : c'est à dire un langage de spécification intégré à des outils de support et à un démontreur de théorème. Il est prévu pour capturer la plus sophistiquée des méthodes formelles mécanisées et pour être suffisamment robuste pour pouvoir être utilisé pour des applications significatives. PVS est un prototype de recherche : il évolue et s'améliore puisque nous développons ou appliquons de nouvelles possibilités, et puisque la charge d'une utilisation réelle expose de nouveaux besoins.

Le but à long terme du groupe de recherche SNePS est la conception et la construction d'un langage naturel utilisant un agent cognitif informatisé, et d'effectuer la recherche dans l'intelligence artificielle, les linguistiques calculatoires, et la science cognitive nécessaire pour cette entreprise. Les trois parties sur lesquelles le groupe met l'accent sont la représentation du savoir, le raisonnement, et la compréhension et la génération du langage naturel. Le groupe est largement connu pour son développement du système de représentation/raisonnement du savoir SNePS, et pour Cassie, son agent cognitif informatisé.

Soar a été développé pour être une architecture cognitive générale. Nous avons l'ultime intension de permettre à l'architecture Soar de :

En d'autres termes, notre intention est de donner à Soar toutes les compétences requises par un agent intelligent général.

TCM (Toolkit for Conceptual Modeling : boîte à outil pour la modélisation conceptuelle) est notre suite d'éditeurs graphiques. TCM contient des éditeurs graphiques pour des diagrammes entité-relation, des diagrammes classe-relation, des diagrammes de flux de données et d'évènements, des diagrammes de transition d'état, des diagrammes de structure de procédé de Jackson et des diagrammes de réseau systèmes, d'arbres de décomposition de fonction et d'éditeurs de tables variés, tels qu'un éditeur de table fonction-entité ou un éditeur de table de décomposition de fonction. TCM est facile d'accès et procède à de nombreuses vérifications de consistance, dont certaines sont effectuées immédiatement, d'autre pendant la requête.

WEKA (Waikato Environnement for Knowledge Analysis : Environement Waikato pour une analyse de connaissance) est la pointe de la technologie des procédures qui appliquent les techniques d'apprentissage de machines à des problèmes pratiques. C'est un banc d'essai logiciel complet qui permet d'analyser les données du monde réel. Il intègre différents outils d'apprentissage machine avec un squelette identique et une interface utilisateur uniforme. Il a été conçu pour accepter une méthode "simplicité prioritaire" qui permet à l'utilisateur d'expérimenter de façon interactive avec un outil d'apprentissage machine simple avant de se tourner vers des solutions plus complexes.