In a now famous paper published in 1976, Nuel Belnap argues that

computer reasoning should be modeled on the basis of a four-valued

logic in which each value is a combination of the two classical

values. Belnap also considers two lattices on these four values, one

corresponding to increase in truth and non-falsity, the other to

increase of information. Together these two lattices form what is now

called a /bilattice/.

More recently Yaroslav Shramko and Heinrich Wansing (2005) have in a

sense repeated Belnap's move, arguing that the logic of the reasoning

of computer /networks/ should be 16-valued, with each value

corresponding to a set of Belnap's values. They consider what is

called a /trilattice/ on these 16 values and distinguish between an

entailment relation based on the notion of truth and one based on

falsity. These two relations are not equal or each other's inverses.

In this talk, which reports on joint work with Stefan Wintein, I will

look at syntactic characterisations of these logics. In particular a

propositional logic will be studied in which all 16-valued truth

functions can be expressed. The logic will be provided with four

semantic consequence relations, one based on truth, one on falsity,

one on approximation, and one on the intersection of the first two. An

analytic signed tableau calculus will then be given that can model

each of these semantic consequence relations in a sound and complete

way. It has the property that a proof in general requires several

tableaux, four tableaux for any of the first three consequence

relations just mentioned, and six for the last. It will be shown how

this calculus generalises a calculus for a functionally complete

variant of Belnap's logic, which in its turn generalises a standard

signed tableau calculus for classical logic. Time permitting I will

also spend a few words on a simple theorem prover implementing the

calculus.