The Logic Refinery Pipeline
How Divergynth transforms dense commercial contracts and complex operational data into unambiguous, First-Order Logic (FOL) formulas evaluated by automated SMT solvers.
Substrate Ingestion & Parsing
Raw agreements and operational data streams are ingested and tokenized under Zero-Knowledge rules, isolating explicit obligations, latent conditions, and warranty disclaimers.
First-Order Logic (FOL) Extraction
Natural language clauses are translated into formal mathematical propositions, mapping entities to uninterpreted functions to strip away rhetorical ambiguity.
CVC5 SMT Adjudication
Formulas are adjudicated through a native Satisfiability Modulo Theories solver. Contradictory terms and unbacked assertions trigger formal logic friction penalties (P_logic).
Domain Verification: Contractual Consistency
Below is the exact QF_UF (Quantifier-Free Uninterpreted Functions) syntax generated when testing whether an "unclassified excavation" risk shift contradicts the owner's geotechnical warranties:
; Divergynth SMT-LIB v2 Formal Constraint Extraction
(set-logic QF_UFLRA)
; Domain Sorts
(declare-sort Condition 0)
(declare-sort Party 0)
; Contractual Entities
(declare-const Subcontractor Party)
(declare-const Owner Party)
(declare-const UnclassifiedBedrock Condition)
; Relational Logic: Cost Assignments and Warranty States
(declare-fun cost-allocation (Condition Party) Real)
(declare-fun warrants-accuracy (Party Condition) Bool)
; Axiom 1 (Schedule B): Owner warrants accuracy of site bore logs
(assert (warrants-accuracy Owner UnclassifiedBedrock))
; Axiom 2 (§4.2): Subcontractor bears all cost > 0 for unclassified rock
(assert (> (cost-allocation UnclassifiedBedrock Subcontractor) 0.0))
; Epistemic Invariant (Precedence): If Owner warrants a site condition,
; the Subcontractor's cost liability for deviations must equal 0.0.
(assert (=>
(warrants-accuracy Owner UnclassifiedBedrock)
(= (cost-allocation UnclassifiedBedrock Subcontractor) 0.0)
))
; Evaluate consistency of the contractual logic model
(check-sat)
; Result: UNSAT
; (Contradiction Isolated: Cost allocation breaks warranty invariant)