Relif: a relation algebra model finder

Relation algebras are algebras arising from the study of binary relations. They form a part of the field of algebraic logic, and have applications in proof theory, modal logic, and computer science. An interesting problem in relation algebras is the so called representation problem, which amounts to give a canonical representation of a given relation algebra, in the form of binary relations. This problem doesn't have a solution for all algebras.

Relif is a specification tool inspired by the Alloy Analyzer that allows the user to explore relation algebras satisfying a set of constraints defined by the user, and provides a way of looking for representations.

Further reading

This project is part of my master's thesis for Software Engineering at Instituto Tecnológico de Buenos Aires. The document describing the theory and motivation behind the tool (as well as its behavior) can be downloaded here. Chapter 3 explains how Relif works, describing its grammar and providing examples.