A Sequent Calculus for Bilattice-Based Logic and Its Many-Sorted Representation

摘要

We introduce a sequent calculus for bilattice-based annotated logic (BAL). We show that this logic can be syntactically and semantically translated into a fragment MSL* of conventional many-sorted logic MSL. We show deductive equivalence of sequent calculus for BAL and sequent calculus for MSL*.