literary pseudonym, Lewis Carroll) introduced the Method of Trees, the earliest modern use of a truth tree. The method of semantic tableaux was invented by the Dutch logician Evert Willem Beth (Beth 1955) and simplified, for classical logic, by Raymond Smullyan (Smullyan 1968, 1995). It is Smullyan's simplification, "one-sided tableaux", that is described above. Smullyan's method has been generalized to arbitrary many-valued propositional and first-order logics by Walter Carnielli (Carnielli 1987). Tableaux can be intuitively seen as sequent systems upside-down. This symmetrical relation between tableaux and sequent systems was formally established in (Carnielli 1991). See also Resolution (logic) References Reprinted in External links TABLEAUX: an annual international conference on automated reasoning with analytic tableaux and related methods JAR: Journal of Automated Reasoning The tableaux package: an interactive prover for propositional and first-order logic using tableaux Tree proof generator: another interactive prover for propositional and first-order logic using tableaux LoTREC: a generic tableaux-based prover for modal logics from IRIT/Toulouse University Logical calculi Automated theorem proving Methods of proof