Software
PρLog is an experimental tool that extends logic programming with strategic conditional transformation rules, combining Prolog with ρLog calculus. It deals with hedges, transforming them by conditional rules. Transformations are nondeterministic and may yield several results. Strategies provide a control on rule applications in a declarative way. The rules apply matching to the whole input hedge (or, if it is a single term, apply at the top position). Four different types of variables give the user flexible control on selecting terms in hedges or subterms in terms. As a result, the obtained code is usually quite short and declaratively clear. Implementation language: Prolog.
- New! Download prholog0.9.zip. Version 0.9 from August 10, 2010. Contains source files and examples. Tested for SWI-Prolog (5.8.0 and later).
Related:
- A short paper on strategies in PρLog.
- A Mathematica implementation of the ρLog calculus.
Flat Matching
Implements the flat matching procedure and its modifications described in this paper. Implementation language: Mathematica.
- Download Flat Matching. Corresponds to the version in the paper. Contains the source code and examples.
- 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.
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.
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.
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.