Skip to main content

find_counterexample

logicaffeine_proof::counterexample

Function find_counterexample 

Source 
pub fn find_counterexample(
    premises: &[ProofExpr],
    goal: &ProofExpr,
) -> Option<Counterexample>
Expand description

Search for a counterexample to premises ⊢ goal: an assignment satisfying every premise while falsifying the goal. None when none is found on the covered fragment (which does NOT prove the goal — absence of a witness here is not a proof).