Skip to main content

ground_problem

logicaffeine_proof::grounding

Function ground_problem 

Source 
pub fn ground_problem(
    premises: &[ProofExpr],
    goal: &ProofExpr,
) -> (Vec<ProofExpr>, ProofExpr)
Expand description

Ground a whole problem — premises AND goal — over the domain of constants they name. The returned premises and goal are quantifier-free (so the kernel proves them, certified, and Z3 decides them instantly).