Autosubst 2 is a tool for the Coq proof assistant which generates syntax to formalize metatheory with binders using parallel de Bruijn substitutions. The tool can generate unscoped and well-scoped de Bruijn syntax from a HOAS input, supporting both polyadic and mondular synax if wanted.
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.