Session Ordered_Resolution_Prover

View theory dependencies
View document
View outline

Theories

Map2
Coinductive.Coinductive_Nat
Coinductive.Coinductive_List
Lazy_List_Liminf
Lazy_List_Chain
Nested_Multisets_Ordinals.Multiset_More
Clausal_Logic
Herbrand_Interpretation
Abstract_Substitution
Inference_System
Ground_Resolution_Model
Unordered_Ground_Resolution
Ordered_Ground_Resolution
Proving_Process
Standard_Redundancy
FO_Ordered_Resolution
FO_Ordered_Resolution_Prover