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.