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.