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:
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 luka contains the sequent rules for the three-valued Lukasiewicz logic as well as several test problems. The demo predicate test/0 loads luka, runs the main routines of MUltseq on all test problems, and writes the output to out.tex, which after running LaTeX on it looks like this.
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 luka contains five test sequents labeled s1 to s5. MUltseq offers the demo predicate test/1 which takes as argument the name of a sequent, runs the main routines on it, and writes the output to out.tex. For example,
?- 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 leftright.
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:
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".