John D. Ramsdell

ocaml-datalog. This package contains a lightweight deductive database system in OCaml

datalog. Datalog interpreter in Lua

agum. Unification and Matching in an Abelian Group

chase. OCaml

gtksudoku. GTK Sudoku eliminates much of the drudgery of solving a Sudoku puzzle and provides educational tips should the path to the solution become obscured.

cmu. Unification in a Commutative Monoid

lineqpp. The Linear Equations Preprocessor solves linear equations and then substitutes the solutions into a document at prescribed locations. It provides linear equation solving capability similar to what is provided by MetaPost, as a general purpose preprocessor. It can be used with SVG to specify the position of graphics objects using a set of linear equations.

cpsa. Cryptographic Protocol Shapes Analyzer (CPSA)