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.
- The results in this paper are discussed in more detail (and also for a different version of sequents) in: Proof Theory of Finite-Valued Logics
- The approach of this paper was generalized in: Labeled calculi and finite-valued logics.
- The MUltlog system will automatically construct many-sided calculi from given truth tables.
Note Errata section at very end for corrected inference rules for the Dunn-Belnap (FDE) system used as an example in the paper.Baaz-et-al-1993-Elimination-of-cuts-in-first-order-finite-valued-logics