-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Logic - truth tables - cardinality - propositional vs sentinal vs predicate vs first order logic decidability validity satisfiable compactness soundness completeness soundness vs completeness (reasoning algorithms) well founded - properties symetric transitive reflexive - first order logic cannot express acyclical graph sentence structures model theory - axiomizable - skolemization validty preserving - unification - deductive tableau - polarity - models finite - resolution theorm prover - Church's theorm - Godel's incompleteness theorm - Lowenheim-Skolem theorm - Peano arithmetic - Presburger arithmetic - variations on natural number structures: Ns vs Nl vs Na vs Nm vs Ne - well founded induction - to review skolemization polarity soundness vs completeness page 292 examples of complete proofs resolution "contains" test tableau assert vs goal converstion to prop logic polarity