Session Weidenbach_Book

Theories

• Multiset
• Multiset_Order
• Multiset_More
• Clausal_Logic
• Herbrand_Interpretation
• Code_Target_Int
• Code_Abstract_Nat
• Code_Target_Nat
• Code_Target_Numeral
• Prop_Logic
• Wellfounded_More
• Prop_Abstract_Transformation
• Prop_Normalisation
• List_More
• Partial_Clausal_Logic
• Prop_Resolution
• Partial_Annotated_Clausal_Logic
• CDCL_NOT
• DPLL_NOT
• DPLL_W
• CDCL_W_Level
• CDCL_W
• CDCL_W_Termination
• DPLL_CDCL_W_Implementation
• DPLL_W_Implementation
• CDCL_W_Implementation
• CDCL_WNOT
• CDCL_W_Incremental
• CDCL_Two_Watched_Literals
• CDCL_Two_Watched_Literals_Implementation
• Prop_Superposition
• Weidenbach_Book