View the project on GitHub
Welcome to the ATBR project website! This project is part of coq-community.
This library provides algebraic tools for working with binary relations. The main tactic provided is a reflexive tactic for solving (in)equations in an arbitrary Kleene algebra. The decision procedure goes through standard finite automata constructions.
Note that the initial authors consider this library to be superseded by the Relation Algebra library, which is based on derivatives rather than automata: https://github.com/damien-pous/relation-algebra
This is an open source project, licensed under the GNU Lesser General Public License v3.0 or later.
The current stable release of ATBR can be downloaded from GitHub.
The coqdoc presentations of releases can be browsed online:
Other related publications, if any, are listed below.