MePo premise selection #
This is a naive implement of the MePo premise selection algorithm, from "Lightweight relevance filtering for machine-generated resolution problems" by Meng and Paulson. It needs to be tuned and evaluated for Lean.
Equations
- Lean.NameSet.instUnion_premiseSelection = { union := fun (s t : Lean.NameSet) => Lean.RBTree.fold (fun (t : Lean.NameSet) (n : Lean.Name) => t.insert n) t s }
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.NameSet.instSDiff_premiseSelection = { sdiff := fun (s t : Lean.NameSet) => Lean.RBTree.fold (fun (s : Lean.NameSet) (n : Lean.Name) => Lean.RBTree.erase s n) s t }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.PremiseSelection.MePo.unweightedScore relevant candidate = Lean.PremiseSelection.MePo.weightedScore (fun (x : Lean.Name) => 1) relevant candidate
Instances For
Equations
- One or more equations did not get rendered due to their size.