MUltseq v2.0-2-gf2ad99b

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. The sequent systems used are the ones described by Baaz, Fermüller, and Zach (1993), Baaz et al. (1998), and Zach (1993).

Multseq 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 by the system; the results can be 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 Gil and Salzer (1999). A “marriage” of MUltlog and MUltseq was described in Baaz et al. (2003). Old versions of MUltseq are still available as gzipped tar archives.

Version 2.0 of Multlog introduces the ability to pre-define properties of a logic and to use the MUltseq prover to test them in a given logic. Properties can be tautologies (e.g., law of excluded middle), consequences (e.g., modus ponens), equivalences (e.g., De Morgan’s laws), quasi-equations (e.g., stating the inter-definability of operators), and meta-consequences (e.g., the deduction theorem).

Installation

MUltseq can be obtained from github.com/rzach/multseq.

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

If you encounter problems, please file an issue.

Examples

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

About MUltseq

MUltseq was originally developed by Àngel Gil (Barcelona) and Gernot Salzer (Vienna) within the framework of an Acción integrada titled “Generic Decision Procedures for Many-valued Logics”. Version 2.0 is joint work with Richard Zach (Calgary)

References

Baaz, Matthias, Christian G. Fermüller, Angel J. Gil, Gernot Salzer, and Norbert Preining. 2003. “MUltlog and MUltseq Reanimated and Married.” In Proceeding 4th International Workshop on the Implementation of Logics, edited by B. Konev and R. Schmidt. Technical Report ULCS-03-018. University of Liverpool. http://www.csc.liv.ac.uk/research/techreports/.
Baaz, Matthias, Christian G. Fermüller, Gernot Salzer, and Richard Zach. 1998. “Labeled Calculi and Finite-Valued Logics.” Studia Logica 61 (1): 7–33. https://doi.org/10.1023/A:1005022012721.
Baaz, Matthias, Christian G. Fermüller, and Richard Zach. 1993. “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.
Gil, A. J., and G. Salzer. 1999. “MUltseq: Sequents, Equations and Beyond.” In Joint Conference of the 5th Barcelona Logic Meeting and the 6th Kurt Gödel Colloquium, 35–36. Barcelona, Spain: https://www.logic.at/multseq/kgc99.pdf.
Zach, Richard. 1993. “Proof Theory of Finite-Valued Logics.” Diplomarbeit, Vienna, Austria: Technische Universität Wien. https://doi.org/10.11575/PRISM/38803.