Elimination of cuts in first-order finite-valued logics
Matthias Baaz, Christian G. Fermüller, Richard Zach · Libraries and Cultural Resources (University of Calgary) · 1994
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.