University of Calgary
UofC Navigation

Elimination of cuts in first-order many-valued logics

This website has moved!

You are looking at an archived page. The website has moved to


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