Type Alias: ProofExportFormat
@kortexya/reasoninglayer / ProofExportFormat
Type Alias: ProofExportFormat
Section titled “Type Alias: ProofExportFormat”ProofExportFormat =
"drat"|"coq"|"lean4"|"isabelle"
Defined in: src/types/proof-engine.ts:477
Target format of an exported refutation certificate.
Remarks
Section titled “Remarks”drat is the native DRAT clausal proof (checkable by drat-trim); coq, lean4
and isabelle are proof scripts for those kernels, emitted by the resolution-
certificate exporters.
Example
Section titled “Example”const format: ProofExportFormat = 'lean4';