Last altered 5/26/12
A problem with presenting logic is that many of the different authors use different symbols and different syntax for the logical expressions. We are just going to choose one (which we think is the best for the present purposes). If you would like something different, that is fine, the software here can run most all systems. Just go to the Preferences page and make your choice. Then the software will run what you would like. Many of the logical symbols look quite similar visually to other symbols, for example the logical 'or' is ∨ and that looks something like capital vee V or even lower case vee v . The software will do everything it can to make sense of your input—but sometimes you just plain have to use the right symbol. You are invited to scan over
These tutorials and
Colin Howson,  Logic with trees ISBN: 0-415-13341-6
would work well together.
You need to know some propositional logic to be able to understand the tutorials to come. In particular, you need to know about the symbols used in propositional logic, truth tables, satisfiability, consistency, and semantic invalidity (by counter example). You do not need to know propositional rules of inference and derivations.
Howson  will give you enough background.
Alternatively you could look at the first five propositional tutorials in Easy Deriver
[The use of trees (or 'tableaux') in logic was pioneered by Beth, Hintikka, and Smullyan, and their use was brought into a teaching context by such books as the standard Jeffrey text. See
E.W. Beth,  The Foundations of Mathematics
G.Gentzen, [1934-5] 'Untersuchungen uber das logische Schliessen', Mathematische Zeitschrift, vol 39, 1934-5, pp.176-210, 405-31
J. Hintikka  ' Two papers on Symbolic Logic', Acta Philosophica Fennica, vol 8 1955
R.C.Jeffrey,  Formal Logic: Its Scope and Limits
R.M. Smullyan,  First Order Logic