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.
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 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.
All software presented within this site are intended for educational and research purposes.
The owners, distributors and any participants disclaim all liability or loss
in conjunction with any content provided here.
Including defective products or direct, indirect, special, incidental or consequential damages,
arising out of the use or the inability to use the materials/information available on this site.