[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

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 documentation.

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
tableau approach.
There is a quick introduction in wikipedia on tableaux:

and the paper is available at
http://projecteuclid.org/Dienst/UI/1.0/Summarize/euclid.ndjfl/ 1093894722?abstract=

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.

Thank you

Clinton R. LeFort

Reply to: