This course is about the handling of logical propositions: read a proposition (in ASCII), make an internal tree representation, calculate the truth table, convert into the disjuctive normal form abd about semantic tableaux.