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.
展开▼