unicode_fol_kit.to_tseitin_cnf¶

unicode_fol_kit.to_tseitin_cnf(node)[source]¶

Return an EQUISATISFIABLE CNF via the Tseitin/definitional encoding.

Unlike to_cnf(), this is not equivalence-preserving: a fresh 0-ary auxiliary predicate Atom is introduced for every compound subformula of the quantifier-free NNF matrix, and the defining biconditionals (aux ↔ op(children)) are expanded into clauses and conjoined with the unit clause asserting the root auxiliary. This avoids the exponential blow-up of the distributive to_cnf() while preserving satisfiability.

The auxiliaries are 0-ary (propositional) definitions, so they only faithfully capture a subformula whose truth value is fixed — i.e. the propositional / ground case the encoding targets. They are not sound inside a quantifier prefix: a single global aux cannot track a subformula such as P(x) whose truth value varies over the domain, which breaks equisatisfiability. This function therefore requires a quantifier-free (after prenexing) input and raises ValueError otherwise.

Parameters:: node (Node)
Return type:: Node