Elimination of cuts in first-order finite-valued logics

Abstract
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.
Description
Keywords
many-valued logic, sequent calculus, Belnap logic
Citation
Baaz, M., Fermüller, C.G., & Zach, R. (1993) Elimination of Cuts in First-order Finite-valued Logics. J. Inf. Process. Cybern. 29(6): 333-355