Theory Selection_Function

theory Selection_Function
  imports Ordered_Resolution_Prover.Clausal_Logic
begin

type_synonym 'a select = "'a clause ⇒ 'a clause"

locale selection_function =
  fixes select :: "'a select"
  assumes
    select_subset: "⋀C. select C ⊆# C" and
    select_negative_literals: "⋀C l. l ∈# select C ⟹ is_neg l"

end