Isabelle/Weidenbach_Book sessions

This session the CDCL calculi (Weidenbach and Nieuwenhuis et al.) and the links between
  both. It also contains a very simple implementation based on lists and two extensions (restart and
  incremental).

  This version is based on the Refinement Framework, to make the two-watched-literals part easier to compile
  (workaround as long as a session cannot have two parents).

This sessions contains the extensions of the CDCL calculus.

This session is the same as the CDCL session, but des not import
  the Refinement Framework.

This session contains various (but still general) definition of entailment used
  later.

We here refine the previous session to generate code.

This extends the previous version to a very simple 'SMT' solver: we enumerate all models and let an unspecified theoty solver checks if a model is valid or another must be found.

This session contains the normalisation from general formulas to CNF and DNF.

This session contains the formalisation of resolution and the beginning of
  superposition.

This session contains all theories related to the two-watched literals. It links
    the abstract CDCL calculus to a more concrete version with watched literals.

We import everything

This session imports HOL, some additional useful theories from HOL, and our own
  extensions above these lemmas.