Session Verified_SAT_Based_AI_Planning

Theories

• List_Supplement
• Map_Supplement
• HOL-Library.Case_Converter
  • File ‹case_converter.ML›
• HOL-Library.Simps_Case_Conv
  • File ‹simps_case_conv.ML›
• Propositional_Proof_Systems.CNF
• Propositional_Proof_Systems.CNF_Sema
• HOL-Library.Old_Datatype
  • File ‹~~/src/HOL/Tools/Old_Datatype/old_datatype.ML›
• HOL-Library.Nat_Bijection
• HOL-Library.Countable
  • File ‹~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML›
• Propositional_Proof_Systems.Formulas
• Propositional_Proof_Systems.CNF_Formulas
• Propositional_Proof_Systems.Sema
• Propositional_Proof_Systems.CNF_Formulas_Sema
• CNF_Supplement
• CNF_Semantics_Supplement
• State_Variable_Representation
• STRIPS_Representation
• STRIPS_Semantics
• SAS_Plus_Representation
• SAS_Plus_Semantics
• SAS_Plus_STRIPS
• List-Index.List_Index
• SAT_Plan_Base
• SAT_Plan_Extensions
• SAT_Solve_SAS_Plus
• AI_Planning_Languages_Semantics.SASP_Semantics
• AST_SAS_Plus_Equivalence
• HOL-Library.Tree
• HOL-Data_Structures.Tree2
• HOL-Data_Structures.RBT
• HOL-Data_Structures.Cmp
• HOL-Data_Structures.Less_False
• HOL-Data_Structures.Sorted_Less
• HOL-Data_Structures.List_Ins_Del
• HOL-Data_Structures.Set_Specs
• HOL-Data_Structures.Isin2
• HOL-Data_Structures.RBT_Set
• HOL-Data_Structures.AList_Upd_Del
• HOL-Data_Structures.Map_Specs
• HOL-Data_Structures.Lookup2
• HOL-Data_Structures.RBT_Map
• HOL-Library.Code_Abstract_Nat
• HOL-Library.Code_Target_Nat
• AI_Planning_Languages_Semantics.SASP_Checker
• HOL-Data_Structures.Set2_Join
• Set2_Join_RBT
• Solve_SASP