Most inconclusive runs are not solved by longer timeouts. They are solved by reading the run report first: cone size, state bits, depth reached, engine progress, and which obligation failed. That measurement chooses among four moves: reduce the model, split the property, strengthen the proof, or, last and documented, justify an assumption. This topic turns that discipline into checklists, and ends with the honest verdict inconclusive, bounded to N.
Lesson | After it you can... |
|---|---|
Classify any run report and pick the matching tactic. | |
Split by value or mode, prove each case, and prove the cases cover everything. | |
Stack lemmas with an audited, cycle-free dependency graph. | |
Call a proof inconclusive with its bound and file the evidence. |
Suggested order: top to bottom. Diagnosis first, because every tactic keys off it. Case splitting second, because it is the commonest structural move. Lemma stacks third, because splits compose into stacks. Stopping last, because it needs the vocabulary of all three to file an honest inconclusive verdict.
Because it changes the model: every assumption narrows the question, and an unjustified one can hide a real bug. Reduction, splitting and strengthening keep the question and change the proof; assumptions change the question and need an owner, a justification and a review.