menu

Return to entry

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

Ordered_Resolution_Prover.Abstract_Substitution

HTML Presentation