Tableaux are a very convenient tool for proofs in classical and non-classical logics, since proof arguments are analyzed instead of synthesized. This seems to be much closer to human reasoning, and to the way humans specify machine reasoning. In this way, tableau methods are much superior than hilbertian methods or natural deduction for software checking, relational and deductive databases and knowledge representation. Tableaux are also philosophically appealing, as they break down the purported duality between syntax and semantics. In many situations, however, natural deduction, sequents and tableau methods can be inter-translated. In this talk I intend to discuss some aspects of such questions and to sketch a general theory of tableau completeness applicable to several non-standard logics and their combinations.