**Autosubst**-
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**-
Satallax is an automated theorem prover for higher-order logic that uses the SAT solver MiniSat.

**Spartacus**-
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**-
Jitpro is an interactive higher-order tableau prover that runs in a web browser.

**Alice**-
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**-
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. **Mozart**-
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.

**XDK**-
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)**-
WSAT(OIP) is a domain-independent local search solver for linear integer constraints.

**DFKI Oz 2**-
(No longer supported.) Oz 2 is the predecessor of Mozart and the successor of Oz 1. For all practical purposes use Mozart.

**DFKI Oz 1**-
(No longer supported.) Oz 1 is an ultra-concurrent constraint programming language. Oz 1 is still available as documentation of how Oz evolved.

**TEL**-
(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.