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.

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.