5 Certificates and verification closure
On this page · Permalink · Source line 408
Definition 5.1: Certificate
A certificate for a nonempty requested target set \(T_0\subseteq V\) is a pair
such that
Order certificates componentwise: \((K,H)\leq(K^{\prime},H^{\prime})\) means \(K\subseteq K^{\prime}\) and \(H\subseteq H^{\prime}\). A least certificate is contained in every certificate for the same request. Minimizing only the node set, only the justification set, or a numerical cost is a different objective.
The usual target request is a subset of \(T\), but an intermediate node may be requested for local analysis. Only a justification whose premises have been derived and whose conclusion is selected can contribute to the derivation. A record may retain other, inactive justifications without using them as proof steps. Extra records cannot lower a nonnegative additive cost, although zero costs can allow several minimizing records.
5.1 The fixed AND-DAG case
On this page · Permalink · Source line 430
The simplest case occurs when each relevant node that is not an admissible leaf has one certified incoming justification. Backward expansion stops at admissible leaves. A proof of a statement that has already been admitted as a leaf is not required to use that statement.
Definition 5.2: AND-DAG
Starting at \(T_0\), expand backward only at nodes outside \(L\). The field is an AND-DAG relative to \(T_0\) when every node reached outside \(L\) has exactly one certified incoming justification. Every premise of that justification is then expanded in the same manner. The process may terminate at an admissible leaf or at a certified justification with no premises.
Let \({\operatorname{Anc}}_L(T_0)\) denote the premise nodes reached by this backward expansion, stopping at \(L\). Let \(H_{\mathrm{core}}\) contain exactly the justifications selected at expanded nodes outside \(L\).
Theorem 5.3: Unique verification core
Let \({\mathcal P}\) be a finite acyclic AND-DAG relative to \(T_0\). Put
Then \((K_{\mathrm{core}},H_{\mathrm{core}})\) is a certificate and is the least certificate under componentwise inclusion. In particular it is the unique inclusion-minimal certificate pair for this recorded inference problem.
Proof
Backward expansion terminates because the dependency graph is finite and acyclic. Every terminal node is either an admissible leaf or the conclusion of the selected justification with no premises. A forward topological pass therefore derives every expanded node. The required premises in \(A\) are admissible and are retained even if the target does not use them. Thus the constructed pair is a certificate.
Now let \((K,H)\) be any certificate for the same request. It contains \(A\cup T_0\). If a requested or required predecessor node is outside \(L\), its derivation must use its unique certified incoming justification. That justification belongs to \(H\), and every one of its premises belongs to \(K\). Repeating the argument forces all of \({\operatorname{Anc}}_L(T_0)\) and \(H_{\mathrm{core}}\). At nodes in \(L\) the argument stops. Hence \(K_{\mathrm{core}}\subseteq K\) and \(H_{\mathrm{core}}\subseteq H\), which proves the least-pair assertion.
Minimizing one coordinate alone does not make the whole record unique. One may add an irrelevant node without changing the least justification set, or retain an unused rule without changing the least node set. The componentwise statement avoids this ambiguity.
Corollary 5.4: Linear extraction
With indexed certified adjacency and constant-time membership bookkeeping, the core can be extracted in time linear in \(|A|\) plus the number of visited nodes, selected justifications, and premise incidences.
This bound concerns the indexed graph algorithm. It is not a verified running-time bound for every scanning routine in the reference Python package.
and_dag.json example. The AND gate requires both \(A\) and \(D\) for \(L_1\). Its least certificate contains five nodes and four certified rules. The gold branch is certified but unnecessary for \(B\). The dashed route to \(F\) is uncertified and cannot enter the certificate.Remark 5.5
The theorem identifies the minimum certificate for the recorded derivation. It does not claim that the derivation is globally shortest among all possible proofs of the theorem. A different proof field may have a smaller core.