We define a satisfiability tree in the context of classical propositional logic.
Satisfiability tree is a structure inspired by the Beth's semantic tableau,
later refined into its modern variant by Lis and Smullyan and by the notion that
tableau is a tree-like representation of a formula.
Basic notions and simple graph operations that correspond to
logical operators are defined for satisfiability trees.
Relation to tableau, parsing trees are investigated.
Clausal satisfiability trees are defined as a class of
satisfiability trees suited for formulas in clausal form.
Issues related to size of clausal satisfiability trees are investigated.
Non-redundant clausal satisfiability trees are shown to be a simple rewrite
of Robinson's refutation trees.