Abstract:
We provide an algorithm that automatically derives many provable theorems
in the equational theory of allegories. This was accomplished by noticing
properties of an existing decision algorithm that could be extended to
provide a derivation in addition to a decision certificate. We also suggest
improvements and corrections to previous research in order to motivate further
work on a complete derivation mechanism. The results presented here
are significant for those interested in relational theories, since we essentially
have a subtheory where automatic proof-generation is possible. This is also
relevant to program verification since relations are well-suited to describe the
behaviour of computer programs. It is likely that extensions of the theory of
allegories are also decidable and possibly suitable for further expansions of
the algorithm presented here.
