nx_fof_tseitin.nx

nx_fof_tseitin.nx -- linear-size FOF -> CNF via Tseitin encoding. Per Vampire-displacement roadmap Phase 2. The naive distribution step in nx_fof_cnf can produce 2^n clauses for n-deep alternations of & and |. Tseitin 1968 introduces a fresh propositional variable p_G for each non-atomic subformula G and asserts the equivalence p_G <-> G as 2-3 clauses. Result: O(n) clauses. Pre-condition: input formula is in NNF and quantifier-free (i.e. post-Skolemize + post-drop_forall). Tseitin doesn't handle IFF or IMP directly -- caller must run elim_iff + elim_imp first (those are also pre-conditions of the existing distribute step). Algorithm: ts_walk(F) returns a Literal that is "true iff F is true". ATOM -> POS atom NEG ATOM-> NEG atom (no fresh var needed) NEG G -> introduce p; emit p <-> ~ts_walk(G) AND L R -> introduce p; recurse on L,R; emit p <-> l_lit & r_lit OR L R -> introduce p; recurse on L,R; emit p <-> l_lit | r_lit Top-level: emit a unit clause asserting ts_walk(F) is true. Equivalence clauses (each ↔ becomes 2-3 clauses): p ↔ ~q : (p ∨ q) ∧ (~p ∨ ~q) p ↔ q ∧ r : (~p ∨ q) ∧ (~p ∨ r) ∧ (p ∨ ~q ∨ ~r) p ↔ q ∨ r : (~p ∨ q ∨ r) ∧ (p ∨ ~q) ∧ (p ∨ ~r) Bits-up nx_int. Tseitin variables get sym_ids in their own range.