Formalizations of clause redundancy properties.

theorem Std.Sat.CNF.entails_clause_of_forall_sat {α : Type u_1} {f : CNF α} {c : Clause α} (h : ∀ (a : α → Bool), Clause.Sat a c) : f.EntailsClause c

We may add any tautological clause

theorem Std.Sat.CNF.entails_clause_of_unsat_of_forall_not_sat {α : Type u_1} {c : Clause α} {f2 f1 : CNF α} (h1 : ∀ (a : α → Bool), ¬Sat a f1 → Clause.Sat a c) (h2 : (f2 ++ f1).Unsat) : f2.EntailsClause c

theorem Std.Sat.CNF.entails_clause_of_unsat_of_isNegationOf {α✝ : Type u_1} {f1 : CNF α✝} {c : Clause α✝} {f2 : CNF α✝} (h1 : f1.IsNegationOf c) (h2 : (f2 ++ f1).Unsat) : f2.EntailsClause c

This is known as the AT or RUP property.

theorem Std.Sat.CNF.exists_sat_add_of_rat {α : Type u_1} [BEq α] [LawfulBEq α] {f : CNF α} {c : Clause α} {l : Literal α} (h1 : l ∈ c) (h2 : ∀ (c' : Clause α), c' ∈ f → l.negate ∈ c' → f.EntailsClause (c ++ c'.erase l.negate)) (a : α → Bool) : Sat a f → ∃ (a' : α → Bool), Sat a' (f.add c)

This is known as the RAT property. It's a formalization of Proposition 1 from "Inprocessing Rules" by Matti Järvisalo, Marijn Heule, and Armin Biere (https://cca.informatik.uni-freiburg.de/papers/JarvisaloHeuleBiere-IJCAR12.pdf)