Map2

Lazy_List_Liminf

Lazy_List_Chain

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