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:
- Report on classical logic
- Report on 3-valued Łukasiewic logic
- Comparing strong and weak Łukasiewic connectives
- Expressing connectives in Łukasiewicz logic
- Experiments in SIXTEEN
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)