icalp-experiments
GitHub指导ICALP论文中证明策略与计算辅助的规范。用于匹配论据与声明，界定SAT/SMT等计算验证定理的合法场景，确保可复现性，并防止将实验性内容混入理论证明。
Trigger Scenarios
Install
npx skills add brycewang-stanford/Awesome-Journal-Skills --skill icalp-experiments -g -y
SKILL.md
Frontmatter
{
"name": "icalp-experiments",
"description": "Use when matching the argument of an ICALP (EATCS) theory paper to its claim — choosing the proof strategy for an upper or lower bound, deciding when supporting computation (SAT\/SMT-verified base cases, computer-assisted case analysis, exhaustive small-case checks) legitimately backs a theorem, and keeping any such computation reproducible without turning a proof paper into an experimental one."
}
ICALP Experiments (proof strategy, and computation in service of proofs)
At ICALP there is usually no experiment section — the evidence for the claim is the proof. This
skill is therefore about matching the argument to the claim shape, and about the narrow, real
cases where computation supports a theorem (a computer-assisted proof, an SMT-checked base case, an
exhaustive small-case verification). It is deliberately not an empirical-evaluation guide: a paper
whose contribution is a benchmark result is mis-routed (icalp-topic-selection).
Match the argument to the claim
| Claim shape | The argument that fits | Common failure caught by referees |
|---|---|---|
| Upper bound / faster algorithm | Algorithm + correctness proof + complexity analysis | Correctness hand-waved; complexity ignores a hidden cost |
| Approximation ratio | An analysis bounding cost vs optimum, with a tight example | Ratio proved only on the easy case; no tight instance |
| Lower bound (unconditional) | A reduction, adversary, or information-theoretic argument | Model too weak to be interesting, or gap left open |
| Conditional lower bound | A fine-grained reduction from SETH/3SUM/APSP | Wrong assumption invoked; reduction loses a factor |
| Decidability / complexity (Track B) | A decision procedure + matching hardness | Procedure sketched; hardness for a different fragment |
| Dichotomy / characterization | Exhaustive case analysis with each case proved | A case silently dropped; "similarly" hiding a hard case |
When computation legitimately supports a theorem
Some ICALP results genuinely rely on computation. It must be rigorous and checkable, not suggestive:
- Exhaustive small-case verification — checking a property for all objects up to size k as a base case of an induction. State the exact range, the encoding, and make the search reproducible.
- SAT/SMT-certified steps — using a solver to verify a finite gadget or unsatisfiability. Ship the encoding and, where possible, an independently checkable certificate (UNSAT proof, Farkas witness), not just "the solver said so."
- Computer-assisted case analysis — a program enumerating cases in a proof. The program is part of the proof; its logic must be described and its output verifiable.
The bar: a referee (or a reader of the full version) must be able to re-run or independently check the computation. A number a solver produced with no reproducible input is not a proof step.
Keep it a proof paper, not an experiment paper
- Supporting computation certifies a step; it does not replace the theorem. If the only evidence for the main claim is "it worked on our instances," the paper is experimental and belongs elsewhere.
- Do not add a benchmark table to a theory paper to look more complete — ICALP referees read it as either irrelevant or as a signal the theorem is weak.
- Running time measured is not running time proved. The contribution is the provable bound.
Reproducibility of the computational part
If computation backs a proof, treat it like the full version (see icalp-reproducibility):
- Provide the code and inputs (or precise pseudocode) in the appendix / full version or a public repository referenced at camera-ready.
- Provide certificates an independent checker can verify where the technique allows.
- Pin versions (solver, seed if randomized search) so the check is deterministic.
Worked vignette: a dichotomy with a computer-checked base
A Track B paper proves a dichotomy over a family of constraint languages: tractable vs NP-hard. The inductive step is by hand; the base cases (finitely many small languages) are verified by an exhaustive program. To meet the bar: state the finite base set precisely, describe the enumeration, ship the code and its output in the full version, and — for the hardness base cases — include reductions a referee can check by hand rather than leaving them to the program alone. State clearly which cases are machine-verified and which are proved analytically.
Output format
[Claim shape] upper / approximation / lower (uncond) / lower (conditional) / decidability / dichotomy
[Argument fit] the proof strategy matches the claim? gaps: <where>
[Computation role] none / base-case check / solver-certified step / computer-assisted cases
[Checkability] certificate or reproducible input provided? independent check possible? yes/no
[Not-an-experiment guard] is the theorem the evidence (not benchmark performance)? yes/no
[Fix queue] <ordered: proof gaps, missing certificates, mis-routed empirical framing>
Version History
- 9f86f09 Current 2026-07-19 15:53
