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.