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