Interface: ProofExportResponse

@kortexya/reasoninglayer / ProofEngine / ProofExportResponse

Interface: ProofExportResponse

Defined in: src/types/proof-engine.ts:568

Response from a certified proof export.

Remarks

certificate is present only when result is unsatisfiable. verified reports whether the engine’s own proof checker re-verified that the certificate derives the empty clause from the input clauses (always false for a non-UNSAT result).

Example

const response: ProofExportResponse = {
  result: 'unsatisfiable',
  format: 'drat',
  certificate: '1 0\n0\n',
  numSteps: 2,
  verified: true,
};

Properties

certificate?

optional certificate: string

Defined in: src/types/proof-engine.ts:574

The exported certificate; absent unless result is unsatisfiable.

format

format: ProofExportFormat

Defined in: src/types/proof-engine.ts:572

The requested certificate format (echoed back).

numSteps

numSteps: number

Defined in: src/types/proof-engine.ts:576

Number of steps in the resolution certificate (0 for a non-UNSAT result).

result

result: ProofExportResult

Defined in: src/types/proof-engine.ts:570

The solver’s verdict.

verified

verified: boolean

Defined in: src/types/proof-engine.ts:578

Whether the engine’s proof checker re-verified the certificate.