MUltlog 1.13 released

MUltlog is a Prolog program that converts a specification of a finite-valued logic (propositional or first-order) into optimal inference rules for a number of related analytic proof systems: many-sided sequent calculus, signed tableaux, many-sided natural deduction, and clause translation calculi for signed resolution. The specification of the logic can be produced by a simple TCL/TK application, iLC (due to Andreas Leitgeb).

MUltlog dates back to 1996 and was written by Gernot Salzer. The code still works, and it turned out that it’s not hard to install it on Linux — all you need is TeXLive and SWI Prolog installed, which is provided packaged in standard distributions like Ubuntu or Debian (as is TCL/TK). I’ve taken Gernot’s code, put it on Github, and gussied it up a little bit. The output of Multlog is a paper that describes the calculi for the system that you input. For instance, below you’ll find the output if you feed it paraconsistent weak Kleene logic.

UPDATE: As of v1.14, the distribution and the new website includes a number of examples, including such favorites as FDE, LP, and classical logic with some fun connectives & quantifiers.

pwk

Here are some other finite-valued logics which were introduced somewhat recently (see www.logic.at/multlog#examples for these and more).

Leave a Reply

Your email address will not be published. Required fields are marked *