A simple algebraic expressions example to demonstrate the basic concepts of abstract syntax tree, symbolic computation, parsing and prettyprinting.

Polymorphic type of formulas with parser and printer.

Binary decision diagrams (BDDs) using complement edges.

Definitional Conjunctive Normal Form.

The Davis-Putnam and the Davis-Putnam-Loveland-Logemann procedures.

Basic stuff for propositional logic: datatype, parsing and prettyprinting, syntax and semantics, normal forms.

Some propositional formulas to test, and functions to generate classes.

Stalmarck method.

Useful functions for handling clauses.

Basic stuff for first order logic: datatype, parsing and printing, semantics, syntax operations and substitution.

Relation between first order and propositional logic; Herbrand theorem.

Model elimination procedure (MESON version, based on Stickel's PTTP).

Some Pelletier problems to compare proof procedures.

Backchaining procedure for Horn clauses, and toy Prolog implementation.

Resolution.

Prenex and Skolem normal forms.

Skolemizing a set of

Tableaux, seen as an optimized version of a Prawitz-like procedure.

Unification for first order terms.

Knuth-Bendix completion.

Congruence closure.

Equality elimination: Brand transform etc.

Naive equality axiomatization.

Simple term orderings including LPO.

Paramodulation.

Rewriting.

Combined decision procedure.

Complex quantifier elimination.

Cooper's algorithm for Presburger arithmetic.

Some decidable subsets of first-order logic.

Geometry theorem proving.

Grobner bases.

Constructive Craig/Robinson interpolation.

Quantifier elimination basics.

Real quantifier elimination.

First-order reasoning by inference.

LCF-style system for first order logic.

LCF implementation of first-order tableaux.

Propositional logic by inference.

Tactics and Mizar-style proofs.

Undecidability.