Consistency Logic Kernel™
Consistency Logic Kernel™
Consistency Logic Kernel™
Deterministic Verification for logical reasoning
Deterministic certification for logical reasoning
Also see the Consistency Math Kernel™
Deterministic certification for mathematics.
CONSISTENCY LOGIC KERNEL™ (CLK)
Deterministic certification for logical correctness in regulated and mission-critical workflows
Public Core Package — Non-Confidential
Overview: what CLK is
The Consistency Logic Kernel™ (CLK) is a deterministic logic certification engine designed to ensure logical correctness in workflows where incorrect reasoning is unacceptable.
CLK runs at inference time as a certification layer and enforces a strict production contract:
CERTIFIED
CLK deterministically validates logical correctness within its supported scope under strict rules.
NOT CERTIFIED
When deterministic certification cannot be established under explicit constraints, CLK fails closed and returns NOT CERTIFIED by design.
Where CLK fits in real systems
CLK is built for workflows where logic must be repeatable, auditable, and safe to automate:
- Certify whether a stated conclusion follows from policy premises (eligibility, compliance, underwriting, audit reasoning).
- Prevent invalid logical inferences from entering regulated records, customer communications, or automated decision engines.
- Guardrail agentic systems: ensure actions are taken only when their preconditions are logically entailed.
- Detect inconsistent rule sets and fail closed instead of producing unsafe decisions.
- Enable safe automation at scale: certified inferences proceed; NOT CERTIFIED triggers retry/reformulate/escalation policies.
How CLK differs from common approaches
CLK is certification-first. It is not a generator, and it is not a general-purpose solver workflow that assumes you will build bespoke encodings. It is designed to sit after generation and enforce a deterministic CERTIFIED-or-NOT CERTIFIED contract in production pipelines.
| Approach (examples) | Correctness guarantee | Failure mode | Integration posture | Best fit |
|---|---|---|---|---|
| LLMs (e.g., GPT/Claude/Gemini) | No deterministic guarantee | Can produce invalid inferences with high confidence | Probabilistic generation | Drafting, exploration, candidate generation |
| SAT solvers (Kissat, CaDiCaL, Glucose, MiniSat) | Strong SAT/UNSAT correctness on CNF encodings | Requires CNF/DIMACS modeling; semantics live in the encoding | Solver engine (CNF backend) | Large-scale SAT/UNSAT classification once encoded |
| SMT solvers (Z3, cvc5, Yices, Boolector) | Strong within supported theories + encodings | Requires precise formal modeling; scope depends on theory support | Formal methods backend (SMT) | Constraint solving, entailment under theories, verification tasks |
| Theorem provers / proof assistants (Lean, Coq, Isabelle) | Highest assurance with explicit proofs | Heavy proof engineering; not optimized for fast inference-time gating | Interactive proof workflow | Formal proofs, specifications, highest-assurance verification |
| Rule engines / logic programming (Datalog, Prolog, ASP) | Strong for rule execution over structured facts | Not a general certify/not certified gate for arbitrary candidate reasoning | Policy/rules execution engine | Deterministic policy evaluation when inputs are already structured |
| CLK™ | Deterministic within certified scope | NOT CERTIFIED when not certifiable (coverage/policy/bounds) | Inference-time certification layer | Correct-or-not certified gating with artifacts + reason codes |
Benchmarks and evaluation results
DeepMind Logic
Deterministic certification of logical entailment: whether a proposed conclusion follows from premises under propositional reasoning.
- 1,696 problems evaluated (1,696 / 1,696)
- 0 incorrect results
- Deterministic decisioning suitable for audit-oriented reasoning pipelines
- NOT CERTIFIED returned when certification cannot be established under strict deterministic rules
SATLIB / DIMACS CNF
Deterministic SAT vs UNSAT classification on DIMACS CNF instances under formal propositional constraints.
- 2,000 instances evaluated (1,000 SAT + 1,000 UNSAT)
- 0 incorrect results (SAT: 1000/1000; UNSAT: 1000/1000)
- Deterministic, reproducible SAT/UNSAT certification
- Strict invariant: wrong must equal zero
Consistency Logic Kernel™ Capabilities
Propositional logic
- Entailment from premises to query (premises ⟹ conclusion)
- CNF satisfiability (SAT/UNSAT) for DIMACS CNF instances
- Wrapper-tolerant parsing for common premises/query formats
Rule-based logic
- Horn-rule entailment (forward chaining)
- Consistency checking for rule sets (fail-closed on inconsistency)
Cardinality / counting constraints
- At-most / at-least / exactly-k style boolean cardinality constraints (within supported scope)
Finite-domain / structured sets
- Finite universe declarations, named sets, membership/containment queries (within supported scope)
Syllogistic reasoning
- All/some/no-style syllogistic patterns (within supported scope)
EUF-style equality reasoning
- Equality/inequality entailment over symbols and uninterpreted functions (ground EUF within supported scope)
- Consistency checking for equality constraints
Also see the Consistency Math Kernel™
Deterministic certification for mathematics.
CONSISTENCY LOGIC KERNEL™ (CLK)
Deterministic certification for logical correctness in regulated and mission-critical workflows
Public Core Package — Non-Confidential
Overview: what CLK is
The Consistency Logic Kernel™ (CLK) is a deterministic logic certification engine designed to ensure logical correctness in workflows where incorrect reasoning is unacceptable.
CLK runs at inference time as a certification layer and enforces a strict production contract:
CERTIFIED
CLK deterministically validates logical correctness within its supported scope under strict rules.
NOT CERTIFIED
When deterministic certification cannot be established under explicit constraints, CLK fails closed and returns NOT CERTIFIED by design.
Where CLK fits in real systems
CLK is built for workflows where logic must be repeatable, auditable, and safe to automate:
- Certify whether a stated conclusion follows from policy premises (eligibility, compliance, underwriting, audit reasoning).
- Prevent invalid logical inferences from entering regulated records, customer communications, or automated decision engines.
- Guardrail agentic systems: ensure actions are taken only when their preconditions are logically entailed.
- Detect inconsistent rule sets and fail closed instead of producing unsafe decisions.
- Enable safe automation at scale: certified inferences proceed; NOT CERTIFIED triggers retry/reformulate/escalation policies.
How CLK differs from common approaches
CLK is certification-first. It is not a generator, and it is not a general-purpose solver workflow that assumes you will build bespoke encodings. It is designed to sit after generation and enforce a deterministic CERTIFIED-or-NOT CERTIFIED contract in production pipelines.
| Approach (examples) | Correctness guarantee | Failure mode | Integration posture | Best fit |
|---|---|---|---|---|
| LLMs (e.g., GPT/Claude/Gemini) | No deterministic guarantee | Can produce invalid inferences with high confidence | Probabilistic generation | Drafting, exploration, candidate generation |
| SAT solvers (Kissat, CaDiCaL, Glucose, MiniSat) | Strong SAT/UNSAT correctness on CNF encodings | Requires CNF/DIMACS modeling; semantics live in the encoding | Solver engine (CNF backend) | Large-scale SAT/UNSAT classification once encoded |
| SMT solvers (Z3, cvc5, Yices, Boolector) | Strong within supported theories + encodings | Requires precise formal modeling; scope depends on theory support | Formal methods backend (SMT) | Constraint solving, entailment under theories, verification tasks |
| Theorem provers / proof assistants (Lean, Coq, Isabelle) | Highest assurance with explicit proofs | Heavy proof engineering; not optimized for fast inference-time gating | Interactive proof workflow | Formal proofs, specifications, highest-assurance verification |
| Rule engines / logic programming (Datalog, Prolog, ASP) | Strong for rule execution over structured facts | Not a general certify/not certified gate for arbitrary candidate reasoning | Policy/rules execution engine | Deterministic policy evaluation when inputs are already structured |
| CLK™ | Deterministic within certified scope | NOT CERTIFIED when not certifiable (coverage/policy/bounds) | Inference-time certification layer | Correct-or-not certified gating with artifacts + reason codes |
Benchmarks and evaluation results
DeepMind Logic
Deterministic certification of logical entailment: whether a proposed conclusion follows from premises under propositional reasoning.
- 1,696 problems evaluated (1,696 / 1,696)
- 0 incorrect results
- Deterministic decisioning suitable for audit-oriented reasoning pipelines
- NOT CERTIFIED returned when certification cannot be established under strict deterministic rules
SATLIB / DIMACS CNF
Deterministic SAT vs UNSAT classification on DIMACS CNF instances under formal propositional constraints.
- 2,000 instances evaluated (1,000 SAT + 1,000 UNSAT)
- 0 incorrect results (SAT: 1000/1000; UNSAT: 1000/1000)
- Deterministic, reproducible SAT/UNSAT certification
- Strict invariant: wrong must equal zero
Consistency Logic Kernel™ Capabilities
Propositional logic
- Entailment from premises to query (premises ⟹ conclusion)
- CNF satisfiability (SAT/UNSAT) for DIMACS CNF instances
- Wrapper-tolerant parsing for common premises/query formats
Rule-based logic
- Horn-rule entailment (forward chaining)
- Consistency checking for rule sets (fail-closed on inconsistency)
Cardinality / counting constraints
- At-most / at-least / exactly-k style boolean cardinality constraints (within supported scope)
Finite-domain / structured sets
- Finite universe declarations, named sets, membership/containment queries (within supported scope)
Syllogistic reasoning
- All/some/no-style syllogistic patterns (within supported scope)
EUF-style equality reasoning
- Equality/inequality entailment over symbols and uninterpreted functions (ground EUF within supported scope)
- Consistency checking for equality constraints
