Elimination of cuts in first-order finite-valued logics

Journal of Information Processing and Cybernetics 29 (1993) 333–355
(with Matthias Baaz and Christian G. Fermüller)

A uniform construction for sequent calculi for finite-valued first-order logics with distribution quantifiers is exhibited. Completeness, cut-elimination and midsequent theorems are established. As an application, an analog of Herbrand’s theorem for the four-valued knowledge-representation logic of Belnap and Ginsberg is presented. It is indicated how this theorem can be used for reasoning about knowledge bases with incomplete and inconsistent information.

Note Errata section at very end for corrected inference rules for the Dunn-Belnap (FDE) system used as an example in the paper.


Approximating propositional calculi by finite-valued logics

24th International Symposium on Multiple Valued Logic. Boston. Proceedings (IEEE Press, Los Alamitos, 1994) 257-263
(with Matthias Baaz)

The problem of approximating a propositional calculus is to find many-valued logics which are sound for the calculus (i.e., all theorems of the calculus are tautologies) with as few tautologies as possible. This has potential applications for representing (computationally complex) logics used in AI by (computationally easy) many-valued logics. It is investigated how far this method can be carried using (1) one or (2) an infinite sequence of many-valued logics. It is shown that the optimal candidate matrices for (1) can be computed from the calculus.

DOI: 10.1109/ISMVL.1994.302193


Note: An extended version is available on arXiv:math.LO/0203204

Proof Theory of Finite-Valued Logics

Diploma Thesis, Technische Universität Wien, Vienna, 1993
Technical Report TUW-E185.2-Z.1-93

Several people have, since the 1950’s, proposed ways to generalize proof theoretic formalisms (sequent calculus, natural deduction, resolution) from the classical to the many-valued case. One particular method for systematically obtaining calculi for all finite-valued logics was invented independently by several researchers, with slight variations in design and presentation. The main aim of this report is to develop the proof theory of finite-valued first order logics in a general way, and to present some of the more important results in this area. This report is actually a template, from which all results can be specialized to particular logics.

The main results of this report are: the use of signed formula expressions and partial normal forms to provide a unifying framework in which clause translation calculi, sequent calculi, natural deduction, and also tableaux can be represented; bounds for partial normal forms for general and induced quantifiers; and negative resolution. The cut-elimination theorems extend previous results, and the midsequent theorem, natural deduction systems for many-valued logics as well as results on approximation of axiomatizable propositional logics by many-valued logics are all new.

DOI: 10.11575/PRISM/38803


Continue reading

Dual systems of sequents and tableaux for many-valued logics

Workshop on Tableau-based Deduction, Marseille, 1993. Bulletin of the EATCS 51 (1993) 192–197 (with Matthias Baaz and Christian G. Fermüller)

The aim of this paper is to emphasize the fact that for all finitely-many-valued logics there is a completely systematic relation between sequent calculi and tableau systems. More importantly, it is shown that for both of these systems there are always two dual proof systems (not just only two ways to interpret the calculi). This phenomenon may easily escape one’s attention since in the classical (two-valued) case the two systems coincide. (In two-valued logic the assignment of a truth value and the exclusion of the opposite truth value describe the same situation.)


Systematic construction of natural deduction systems for many-valued logics

23rd International Symposium on Multiple Valued Logic. Sacramento. Proceedings (IEEE Press, Los Alamitos, 1993) 208–213
(with Matthias Baaz and Christian G. Fermüller)

A construction principle for natural deduction systems for arbitrary finitely-many-valued first order logics is exhibited. These systems are systematically obtained from sequent calculi, which in turn can be automatically extracted from the truth tables of the logics under consideration. Soundness and cut-free completeness of these sequent calculi translate into soundness, completeness and normal form theorems for the natural deduction systems.

DOI: 10.1109/ISMVL.1993.289558


Extended version (appeared as technical report TUW-E185.2-BFZ.1-93)


The MUltlog system will automatically construct many-sided calculi from given truth tables.

Algorithmic structuring of cut-free proofs

Computer Science Logic. 6th Workshop, CSL ’92. San Miniato. Selected Papers (Springer, Berlin, 1993) 29-42
(with Matthias Baaz)

We investigate the problem of algorithmic structuring of proofs in the sequent calculi LK and LKB (LK where blocks of quantifiers can be introduced in one step), where we distinguish between linear proofs and proofs in tree form.

In this framework, structuring coincides with the introduction of cuts into a proof. The algorithmic solvability of this problem can be reduced to the question of k/l-compressibility: “Given a proof of \(\Gamma \vdash \Delta\) of length k, and l < k: Is there is a proof of \(\Gamma \vdash \Delta\) of length < l?” When restricted to proofs with universal or existential cuts, this problem is shown to be

  1. undecidable for linear or tree-like LK-proofs,
  2. undecidable for linear LKB-proofs, and
  3. decidable for tree-like LKB-proofs.

(1) corresponds to the undecidability of second order unification, (2) to the undecidability of semi-unification, and (3) to the decidability of a subclass of semi-unification.

DOI: 10.1007/3-540-56992-8_4