Software

SToUT

In the SToUT project, a library of unification and anti-unification algorithms has been developed. Besides, useful subalgorithms for (constructively) deciding alpha-equivalence and equivariance have been implemented. The library can be accessed from the project Web page. Implementation language: Java. Developer: Alexander Baumgartner.

PρLOG

PρLog is an experimental tool that extends logic programming with strategic conditional transformation rules, combining Prolog with ρLog calculus. A dedicated page contains more information about it. The tool can also be downloaded from there.

Flat Matching

Implements the flat matching procedure and its modifications described in this paper. Implementation language: Mathematica.

Solver for Well-Moded Regular Constraints

Implements an algorithm for solving well-moded regular constraints. The constraints consist of equational and membership constraint parts built over the alphabet of flexible arity function symbols and individual, sequence, function, and context variables. Subsumes matching with regular constraints described below. Implementation language: Prolog.

  • Download rwcs.zip. Contains a source file rwcs.pl and a file Examples.txt with test examples. Tested for SWI-Prolog (5.4.7 and later). Should run on GNU-Prolog (1.2.16), BinProlog (11.2), and on LPA Win-Prolog (4.600) as well.
  • Licensing: GNU Lesser General Public License (LGPL).

Matching with Regular Constraints

Implements an algorithm for solving context sequence matching problems with regular constraints. Implementation language: Prolog.

  • Download csmrc.zip. Contains a source file csmrc.pl and a file Examples.txt with test examples. Tested for SWI-Prolog (5.4.7 and later) and GNU-Prolog (1.2.16). Should run on BinProlog (11.2) and on LPA Win-Prolog (4.600) as well.
  • Download csmrc-swi.zip. For SWI-Prolog (5.4.7 and later) only. Source is split into modules.
  • Licensing: GNU Lesser General Public License (LGPL).

Theorema Packages

The following packages are part of the Theorema system. They are implemented in Mathematica (4.0 and later):

Constraint Solver for Strict Polynomial Inequalities

Developed in the project "Proving and Solving over the Reals". Implements the generalized bisection method. Implementation language: C. Not maintained anymore.