Session GCR

Theories

Fundamentals

• Tree_Automata_Utils
• Basic_Utils
• Ground_Terms
• GTT

GCR vs. CR

• Ground_Confluence
• LLRG_Confluence
• Monadic_Confluence

GTT and RR_n constructions

• RRn_Automata
• GTT_RRn
• GTT_Compose
• GTT_Transitive_Closure
• GTT_TRS
• TRS_GTT
• LV_to_GTT

Executable code

• GTT_Impl
• Horn_Inference
• Horn_List
• Refine_Iterator
• Horn_Autoref
• GTT_Compose_Impl
• GTT_Transitive_Closure_Impl
• GTT_TRS_Impl
• GTT_RRn_Impl
• LV_to_GTT_Impl
• TA_Simplify_Impl
• Ground_Confluence_Impl
• LLRG_Confluence_Impl