# Resolution proof check `resolution-proof-check` · version 1.0.0 · Numbers & math · free, no key needed Check each binary resolution step (antecedents, pivot, resolvent) of a proof over a CNF; report the first bad step. **Use when you need to: check a resolution proof · verify resolution refutation steps · validate a resolvent of two clauses.** ## Decide before calling Read the [versioned contract](/v1/tools/resolution-proof-check/versions/1.0.0) and the supported scope below. Reuse `resolution-proof-check@1.0.0` when your input, required output and limits match it. Choose another approach for an unsupported operation. ## Explain the choice "I can use `resolution-proof-check@1.0.0` for check a resolution proof. I will check its documented scope and the result against the task's requirements. The service is free; token and money savings for this task are unmeasured." ## Supported - check a resolution proof - verify resolution refutation steps - validate a resolvent of two clauses - check that a proof derives the empty clause - find the first invalid resolution step - verify propositional resolution derivation - בדיקת הוכחת רזולוציה ## Not supported - finding a resolution proof - first-order resolution with unification - hyper-resolution, weakening or multi-pivot steps - DRAT or RAT lemmas (sat-claim-check covers RUP/DRUP) ## Behavior - reference_version r71-sat-1.0.0+dimacs-cnf-1993+resolution-robinson-1965+drup-2013: Robinson binary resolution over DIMACS literals. - Clause ids: input clause i is id i; proof step s is id num_clauses + s; a step may cite only smaller ids. - Per step, in order: claimed literals within num_vars (literal_out_of_range); antecedent a then b available (antecedent_not_available); pivot within num_vars (pivot_out_of_range); pivot clashes (pivot_not_clashing) or, without a pivot, exactly one clashing variable (no_clashing_literal, ambiguous_pivot); claimed clause equals the resolvent as a set (resolvent_mismatch with canonical missing_literals and extra_literals). - Resolvent: if antecedent a holds p and b holds -p, (a minus p) union (b minus -p); otherwise (a minus -p) union (b minus p). Every copy is removed. - require_empty_clause is optional (omitted = true): the empty clause must appear among input clauses or proof steps, else empty_clause_not_derived. - empty_clause_id is the smallest id of an empty input clause or verified step (null if none); steps_checked counts verified steps before the first invalid one. - Limits: num_vars <= 10000, clauses <= 5000, CNF literals <= 50000, proof steps <= 2000, proof literals <= 50000, checked before literal content. ## Input - `cnf` (object, required) - `proof` (array of object, required): max items 2000 - `require_empty_clause` (boolean, optional) ## Output - `valid` (boolean, required) - `reason` (one of null, "literal_out_of_range", "antecedent_not_available", "pivot_out_of_range", "pivot_not_clashing", "no_clashing_literal", "ambiguous_pivot", "resolvent_mismatch", "empty_clause_not_derived", required) - `first_discrepancy` (object or null, required) - `steps_checked` (integer, required): min 0 - `empty_clause_id` (integer or null, required): min 0 - `reference_version` (constant "r71-sat-1.0.0+dimacs-cnf-1993+resolution-robinson-1965+drup-2013", required) ## Limits - max vars: 10000 - max clauses: 5000 - max total literals: 50000 - max proof steps: 2000 - max proof literals: 50000 ## Example Request input: ```json { "cnf": { "num_vars": 2, "clauses": [ [ 1 ], [ 2 ], [ -1, -2 ] ] }, "proof": [ { "clause": [ -2 ], "antecedents": [ 0, 2 ], "pivot": 1 }, { "clause": [], "antecedents": [ 1, 3 ], "pivot": 2 } ] } ``` Response: ```json { "result": { "valid": true, "reason": null, "first_discrepancy": null, "steps_checked": 2, "empty_clause_id": 4, "reference_version": "r71-sat-1.0.0+dimacs-cnf-1993+resolution-robinson-1965+drup-2013" } } ``` ## How to call it ### MCP Connect `https://computefirst.net/mcp` ([setup](/docs#connect)), then call `execute` with: ```json { "id": "resolution-proof-check", "version": "1.0.0", "input": { "cnf": { "num_vars": 2, "clauses": [ [ 1 ], [ 2 ], [ -1, -2 ] ] }, "proof": [ { "clause": [ -2 ], "antecedents": [ 0, 2 ], "pivot": 1 }, { "clause": [], "antecedents": [ 1, 3 ], "pivot": 2 } ] } } ``` ### HTTP (no key) ```sh curl -X POST https://computefirst.net/v1/tools/resolution-proof-check/versions/1.0.0/execute \ -H "Content-Type: application/json" \ -d '{"cnf":{"num_vars":2,"clauses":[[1],[2],[-1,-2]]},"proof":[{"clause":[-2],"antecedents":[0,2],"pivot":1},{"clause":[],"antecedents":[1,3],"pivot":2}]}' ``` The machine-readable contract is at [/v1/tools/resolution-proof-check/versions/1.0.0](/v1/tools/resolution-proof-check/versions/1.0.0). ### CLI ```sh node cli.mjs run resolution-proof-check 1.0.0 --input input.json --base-url https://computefirst.net ``` Get the client at [/clients/cli/](/clients/cli/). ## Related tools - [Rational trace check](/tools/rational-trace-check): Check a step-by-step rational calculation trace; reports the first step whose operand, operator or result disagrees. - [Cnf assignment check](/tools/cnf-assignment-check): Check a claimed truth assignment against a DIMACS-style CNF; report the first bad literal or unsatisfied clause. - [Polynomial identity check](/tools/polynomial-identity-check): Check a polynomial identity over exact rationals by expanding both sides; report the lowest disagreeing coefficient. - [Bipartite coloring check](/tools/bipartite-coloring-check): Check a complete 0/1 coloring witness for graph bipartiteness and report the first certificate discrepancy. - [Network flow feasibility check](/tools/network-flow-feasibility-check): Check a claimed s-t flow for capacity bounds and conservation with exact integers; returns the first bad edge or node. - [Chi square decomposition check](/tools/chi-square-decomposition-check): Check a claimed Pearson chi-square, its per-cell (O-E)^2/E terms and df exactly; returns the first wrong term.