pub fn discharge_unary_facts(premises: &[ProofExpr]) -> Vec<ProofExpr>Expand description
Discharge known ground UNARY facts (Trip(Alpha), …) throughout the premises:
each is true, so replace it with True and simplify True ∧ X ↦ X,
True → X ↦ X. Unit propagation on the sort facts — it strips the sort guards out
of every grounded clause ((Trip(x) ∧ In(x,FL)) ∧ … ↦ In(x,FL) ∧ …, and a closure
Trip(t) → D ↦ D becomes a bare disjunction fact), leaving the pure value-literal
clauses propagation runs on in ONE step. Sound: a true conjunct/antecedent carries
no information.