Temur Kutsia

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), developed in the project SQUEE.

• Download mmpt.zip. Implementation language: SWI-Prolog.
• Licensing: GNU Lesser General Public License (LGPL).

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

• Download Flat Matching with finite representation of solution sets. A version that, in addition to the version in the paper, implements also finite representation of solution sets. Contains the source code and examples. Version 0.1.
• Licensing: GNU Lesser General Public License (LGPL).

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

• Equational Prover of Theorema. Detailed description.
• Theorema Interface with External Systems. Detailed description.
• Unification with Higher-Order Patterns. Implements Nipkow's modification of Miller's algorithm.
• Unification with Sequence Variables. Detailed description. This procedure is implemented also in RhoLog.
• Translation of the TPTP library into Theorema syntax.

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.