MUltlog 1.17 & iLC 1.2

MUltlog is a system which takes as input the specification of a finitely-valued propositional or first-order logic and produces a sequent calculus, tableau and natural deduction systems, and clause formation rules for this logic. The output is in the form of a scientific paper written in LaTeX.

The systems produced are the ones described by Baaz, Fermüller, and Zach (1993b), Baaz, Fermüller, and Zach (1993a), Baaz, Fermüller, and Zach (1993c), Zach (1993). All generated rules are optimized regarding their branching degree as described by Salzer (2000). The system was first presented by Salzer (1996).

MUltlog is written in Prolog, and should run with any standard interpreter (tested with SWI- and SICStus-Prolog). The input to MUltlog can be created with any text editor. Viewing the generated paper requires the LaTeX typesetting system.

iLC, the interactive Logic Creator, offers a graphical user interface (written in a Tcl/Tk) for producing logic specification files for use with MUltlog.

The experimental “interactive mode” lets you investigate many-valued logics: find tautologies, check for entailment, define products and factors of logics, or test for isomorphisms.

Installation

MUltlog can be obtained from github.com/rzach/multlog.

For installation instructions, see the MUltlog user manual (also available in PDF).

If you encounter problems, please file an issue on GitHub.

Examples

A number of example of logic specifications are provided in the examples directory. They result in the following PDFs:

About MUltlog

MUltlog is a project by the Vienna Group for Multiple-valued Logics, supported by FWF grant P10282-MAT (Austrian Science Foundation). The people that contributed to MUltlog are (in alphabetical order):

  • Stefan Katzenbeisser: rewrote (together with Stefan Kral) the optimization procedure for operators using more efficient data structures.
  • Stefan Kral: see Stefan Katzenbeisser.
  • Andreas Leitgeb: author of iLC (interactive Logic Creator), a window-oriented interface to MUltlog.
  • Wolfram Nix: author of eLK, a menu-oriented DOS interface to MUltlog (no longer available).
  • Alexandra Pascal: author of JMUltlog, a Java-based web interface to MUltlog (no longer available).
  • Gernot Salzer: author of the MUltlog kernel and coordinator of the project.
  • Markus Schranz: author of the HTML/Perl-based web interface to MUltlog.
  • Richard Zach: updated the LaTeX code for the 25 anniversary, included tableaux systems and (optional) explicit sequents in the LaTeX output, and implemented the “interactive mode.”

References

Baaz, Matthias, Christian G. Fermüller, and Richard Zach. 1993a. “Dual Systems of Sequents and Tableaux for Many-Valued Logics.” Bulletin of the EATCS 51: 192–97. https://doi.org/10.11575/PRISM/38908.
———. 1993b. “Elimination of Cuts in First-Order Finite-Valued Logics.” Journal of Information Processing and Cybernetics EIK 29 (6): 333–55. https://doi.org/10.11575/PRISM/38801.
———. 1993c. “Systematic Construction of Natural Deduction Systems for Many-Valued Logics.” In 23rd International Symposium on Multiple-Valued Logic. Proceedings, 208–13. Los Alamitos: IEEE Press. https://doi.org/10.1109/ISMVL.1993.289558.
Salzer, Gernot. 1996. “MUltlog: An Expert System for Multiple-Valued Logics.” In Collegium Logicum, 50–55. Vienna: Springer. https://doi.org/10.1007/978-3-7091-9461-4_3.
———. 2000. “Optimal Axiomatizations of Finitely Valued Logics.” Information and Computation 162 (1–2): 185–205. https://doi.org/10.1006/inco.1999.2862.
Zach, Richard. 1993. “Proof Theory of Finite-Valued Logics.” Diplomarbeit, Vienna, Austria: Technische Universität Wien. https://doi.org/10.11575/PRISM/38803.