MUltseq is a program that can be used to decide the validity of
finitely-valued formulas, the consequence relation, and the validity
of equations and quasi-equations in certain finite algebras.
In its core, MUltseq is
a generic sequent prover for propositional finitely-valued logics. It is
intended as companion for MUltlog
which computes optimized sequent rules from the
truth tables of a finitely-valued logic.
MUltseq uses these rules to construct derivations - automatically or
interactively - for sequents given directly by the user or generated from the
(quasi-)equations; the results are typeset using LaTeX.
A short description of MUltseq
was presented at the *"Joint conference of the 5th Barcelona Logic Meeting and
the 6th Kurt Gödel Colloquium"* in June 1999 (see also
the slides);
a longer version will appear in 2001.

**Contents of this page:**

MUltseq currently is at version 0.6 (13/09/2002) and consists of the following parts:

`mscalcul.pl`: proof construction and transformations-
`msconf.pl`: OS- and Prolog-specific settings `msconseq.pl`: transforms (quasi-)equations, formulas, and consequence relations on sequents and formulas to equivalent sets of sequents`mslgcin.pl`: routines for reading the specification of a sequent calculus (for an example of such a specification see luka)`msoption.pl`: option processing`mstex.pl`: output routines (TeX)`msutil.pl`: auxiliary predicates`multseq.pl`: main file; loads the other parts of MUltseq listed above`mspost.tex`: postamble of TeX documents created by MUltseq`mspre.tex`: preamble of TeX documents created by MUltseq`proof.sty`: style file for typesetting derivations (by Makoto Tatsuta)`luka`: specification of a sequent calculus for the three-valued Lukasiewicz logic

MUltseq is written in Prolog and should run with any standard interpreter. A free Prolog system is SWI-Prolog by Jan Wielemaker.

The output of MUltseq is formatted as LaTeX document. LaTeX is a scientific typesetting system freely available from any CTAN host (e.g. ftp.dante.de or ftp.tex.ac.uk) or one of its mirrors.

This section describes a demo session with MUltseq 0.6.
As first step we start Prolog and load the program MUltseq consisting of
all files with extension `pl`.

% pl Welcome to SWI-Prolog (Version 3.2.8) Copyright (c) 1993-1998 University of Amsterdam. All rights reserved. For help, use ?- help(Topic). or ?- apropos(Word). ?- [multseq]. msconf compiled, 0.00 sec, 808 bytes. msutil compiled, 0.00 sec, 12,896 bytes. mscalcul compiled, 0.02 sec, 19,320 bytes. msconseq compiled, 0.00 sec, 13,272 bytes. mslgcin compiled, 0.02 sec, 14,032 bytes. msoption compiled, 0.00 sec, 5,440 bytes. mstex compiled, 0.02 sec, 72,168 bytes. multseq compiled, 0.08 sec, 149,008 bytes. Yes ?- test.The file

For details on how to call the main predicates of MUltseq see the implementation
of `test/0` in the file
`multseq.pl`.
The available options are essentially the same as in MUltseq 0.4 (see below).

This section describes a demo session with MUltseq 0.4. The experiments were done with SWI-Prolog under Unix.

As first step we start Prolog, load the program MUltseq consisting of
all files with extension `pl`, and read the sequent rules
for the three-valued Lukasiewicz logic, which are provided in the text file
`luka`.

% pl Welcome to SWI-Prolog (Version 2.9.10) Copyright (c) 1993-1997 University of Amsterdam. All rights reserved. For help, use ?- help(Topic). or ?- apropos(Word). ?- [multseq]. msconf compiled, 0.00 sec, 904 bytes. mskernel compiled, 0.00 sec, 19,992 bytes. mslgcin compiled, 0.02 sec, 7,224 bytes. msoption compiled, 0.00 sec, 5,544 bytes. mstex compiled, 0.02 sec, 32,144 bytes. msutil compiled, 0.00 sec, 6,000 bytes. multseq compiled, 0.03 sec, 74,456 bytes. Yes ?- load_logic(luka).The file

?- test(s1).produces this plain text file, which after running LaTeX on it looks like this.

By default, MUltseq represents many-valued sequents as lists of signed formulas. Optionally, MUltseq can also output multi-dimensional sequents. The commands

?- set_option(tex_sequents(multidimensional)). ?- test(s1).yield the same derivations as above, but in a different style. Further options control the amount of additional information added to derivations, like names of applied rules.

For a given sequent there are usually several applicable rules. Which one is selected depends on the chosen strategy. MUltseq currently offers three automatic strategies (meaning that it selects the rules without intervention by the user) and one interactive strategy. In the latter case the user is asked for his/her choice whenever several rules apply.

?- set_option(strategy(interactive)). ?- test(s1). Sequent: [ (a=>b)^p, (a v c)^t] 1: rule ip yields the premise(s) [a^p, b^p, (a v c)^t] [a^t, b^f, (a v c)^t] 2: rule ot yields the premise(s) [ (a=>b)^p, a^t, c^t] Your choice: 2.The output of this run differs from the previous one, which used the default strategy

Here is the output generated by running `test/1`
on the other test sequents in `luka`
with default settings:
`s2`,
`s3`,
`s4`, and
`s5`.
The last example shows the necessity of automatic proof structuring tools:
rather small sequents may lead quickly to derivations which are
too wide for an ordinary sheet of paper, even when representing sequents
by numbers. Such tools are on the agenda for upcoming versions of MUltseq.

Here is a list of ideas, which could/should/must be implemented:

- Automatic proof structuring tools (see the discussion of example
`s5`above). - A user-friendly, window-oriented interface for MUltseq, e.g. for editing many-valued sequents (possible languages: Tcl/Tk, HTML/Java, XPCE).
- Specification of sequent calculi: separation of the logical content (sequent rules) from the TeX-related parts in the input file. The idea is to shift as much of the TeX-formatting stuff as possible to a style file.
- More possibilities for user interaction during proof search, like introduction of cuts.
- Interface to MUltlog: MUltlog has to output the sequent calculus in a form suitable for MUltseq.
- Pruning of derivations: remove parts of proofs, which derive signed formulas which could also have been introduced by weakening; amounts to restructuring the proof such that axioms are reached as soon as possible.
- Reuse of proofs: keep already proved sequents in a minimized form and reuse them whenever a super-sequent (a sequent containing some already proved sequent) has to be proved; amounts to regarding proved sequents as new axioms.
- Improved TeX formatting, to allow e.g. page breaks in the table of sequents.

MUltseq is jointly developed by
Angel Gil (Barcelona) and
Gernot Salzer (Vienna)
within the framework of an *Acción integrada*
titled "Generic Decision Procedures for Many-valued Logics".