### The Metamorpho system

Metamorpho is a system which can perform various kinds of symbolic manipulation related to the calculus of relations. In particular, it supports various translations across logical formalisms (from the calculus of relations to first-order predicate calculus; from three-variable formulae of first-order calculus into the calculus of relations, from non-classical logics into the calculus of relations, etc.). It also supports various mechanisms for extending the language of relation algebras.

### Basic laws on relations proved automatically with Otter

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.

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" by Alfred Tarski and Steven Givant), 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.

Common approaches to the automation of modal inferences often exploit*transIt*: A Prolog tool for relational translation of modal logics*ad hoc*, direct inference methods. We pursue an alternative approach, aimed at developing a uniform relational platform for modal reasoning, which is intended to benefit from relational renderings of non-classical logics.

The envisaged framework consist in a full-fledged inferential apparatus, where the inferential activity can be seen as decomposed into two steps. First, a translation phase brings from one (propositional) modal formalization of a problem to its relational formulation. Then, a deductive method is exploited, within the relational context, in order to seek for a proof.

We are developing a prototypical implementation of a Prolog-based tool able to uniformly translate sentences from various modal logics into the calculus of binary relations.

At the moment the Prolog translator is able to produce relational renderings of several modal logics (among others, lattice-based modal logics, logics of knowledge and of information, intuitionistic logic, etc).

Extensions of the tool are currently under development and including the treatment of further logics, as well as the integration of semi-automated deduction tools.

andy Last update 2016-11-03