University of Calgary
UofC Navigation

Elimination of cuts in first-order many-valued logics


Journal of Information Processing and Cybernetics 29 (1994) 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: The approach of this paper was generalized in: Labeled calculi and finite-valued logics.

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


Download PDF