Re: Molle? To Michele Mazzucchi of Politecnico di Milano
On 05/feb/07, at 02:23, clefort wrote:
Recently I came across the program which is credited to "Molle has
been developed by Michele Mazzucchi and Andrea Mocci as a project
for the course in advanced logics at Politecnico di Milano, under
the supervision of Prof. Marco Colombetti and Prof. Alessandra
Cherubini." I am using the program quite alot lately. I am
interested to know of what models or references you used to develop
your system. I think M. Fitting was mentioned at one point in the
Thanks for your interest.
Melvin Fitting published the algorithm which is used by Molle for
proving modal formulae.
It is an extension to modal logics of the "analytic tableaux"
algorithm. It uses the implicit
There is a quick introduction in wikipedia on tableaux:
and the paper is available at
I am particularly interested in what is called deontic logic. Will
there be further documentation to Molle?
we did not and will not ever include documentation about the actual
algorithm itself, which
can be explored in the scientific literature.
Besides internals, we designed and account the GUI to be fully usable
without any documentation on it.
Nonetheless, Molle will feature a quick tutorial documentation as
soon as all the extra frame properties
will be implemented.
What are the plans for the development of Molle at this time?
Improvements have been done wrt the release of Molle which is
publicly available, mostly towards
frame properties. However, development is currently very idle and we
do not expect to achieve a release
before a few months.
Presently I am reading B. Cellas, M. Fitting and Hughes & Cresswell.
Clinton R. LeFort