Translating First-Order Predicate Logic to Relation Algebra, Implemented Using Z3

This stand-alone Python tool is an implementation of the translation from First-Order Predicate Logic to Relation Algebra that can be run independently so that it can be of use to any tool that takes Relation Algebra as its input language. We made the implementation highly readable to encourage re-implementation into other tools as well. Also included is a simplification tool for reducing Relation Algebra formulas. This implementation also contains a simplification tool that was generated with the help of Z3 for reducing Relation Algebra formulas.