### Basic laws on relations proved automatically with Otter

Andrea Formisano, Eugenio G. Omodeo

Department of Computer Science,

University of L'Aquila (Italy)

An experimentation on automated reasoning in the calculus of
relations was undertaken by the authors a few years ago.

Originally, the main motivation for this activity was to carry out
a comparison between the performances of a theorem prover in the realm
of Set Theory when the axioms of ZF are provided in their traditional
first-order formulation, and when they are recast in purely equational
terms. We felt free to customize the axioms on dyadic relations in ways
that would enhance the deduction process, but nevertheless a significant
part of the experimentation was absorbed by proofs regarding the
calculus of relations *per se*.

In sight of wider exploitations of the calculus of relations (e.g.,
for automated reasoning in non-classical logics), we began to feel the
need to assess once and for all how well a standard theorem prover,
namely Otter, could cope with the calculus of relations. Accordingly,
we began to derive systematically algebraic laws on relations, without
indulging any longer to our own taste to select the axioms. We referred
to a classical monograph on the subject, namely "A Formalization of Set
Theory without Variables", both to choose the axioms and to single out
a significant benchmark. Specifically, pages 49-50 of that monograph
provide a catalog of crucial laws which we have submitted as goal
theorems to Otter. It turned out useful, to speed up some of the proofs,
to enrich the catalog variously, e.g. by including in it the Dedekind law.

We believe that our series of experimental results, after revisions
aimed at setting up a structured library of algebraic laws and rules,
can become a useful reference for any researcher in relational logics.