Skip to main content

grid_prove

Function grid_prove 

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

Solve a single grid cell by propagation and emit its certified derivation. The premises must be ground (call grounding::ground_problem first). Returns None when the cell is not forced by propagation alone (it needs search — Phase C) or the premises do not classify as a grid.