Autosubst is a library for the Coq proof assistant to formalize metatheory with binders using parallel de Bruijn substitutions. It features a decision procedure for equations containing substitution applications.
Satallax is an automated theorem prover for higher-order logic that uses the SAT solver MiniSat.
Spartacus is a tableau prover for hybrid logic with global modalities. It uses pattern-based blocking for termination and implements a number of optimizations.
Jitpro is an interactive higher-order tableau prover that runs in a web browser.
Alice is a functional programming language based on Standard ML, extended with support for concurrent, distributed, and constraint programming. Alice extends Standard ML with laziness, futures, higher-order modules, components, packages, pickling, and constraints.
Gecode is the Generic Constraint Development Environment, a C++ constraint library. It is a research platform for investigating new implementation techniques for constraint systems. Gecode is developed jointly with KTH, Sweden.
The Mozart Programming System is an advanced development platform for intelligent, distributed applications. Mozart is based on the Oz language, which supports declarative programming, object-oriented programming, constraint programming, and concurrency as part of a coherent whole.
The XDG Development Kit (XDK) is a grammar development environment for the meta grammar formalism of Extensible Dependency Grammar (XDG). It includes a constraint-based parser, a graphical user interface, lots of example grammars, and extensive documentation.
WSAT(OIP) is a domain-independent local search solver for linear integer constraints.
(No longer supported.) Oz 2 is the predecessor of Mozart and the successor of Oz 1. For all practical purposes use Mozart.
(No longer supported.) Oz 1 is an ultra-concurrent constraint programming language. Oz 1 is still available as documentation of how Oz evolved.
(No longer supported.) TEL, an acronym for types, equations and logic, is a second generation logic programming language. It is the practical outcome of a research effort aimed at the integration of types and functions with logic programming à la Prolog.