Matching modulo Proximity Theories

Experimental version of a matching algorithm modulo a special kind of proximity theories (cf. matching modulo equational theories vs matching modulo proximity theories).

Library of Unification and Anti-Unification Algorithms

In the projects SToUT and GALA, a library of unification and anti-unification algorithms has been developed. Besides, useful subalgorithms for (constructively) deciding alpha-equivalence and nominal equivariance have been implemented. The library can be accessed from its Web page. Implementation language: Java. Main 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.

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).