Function to_nnf 

pub fn to_nnf(expr: &TLExpr) -> TLExpr

Convert an expression to Negation Normal Form (NNF).

NNF is a normalized form where:

• Negations are pushed inward to appear only before predicates
• Implications are eliminated
• Only AND, OR, NOT (before predicates), predicates, and quantifiers remain

This is an intermediate step for CNF/DNF conversion.

Examples

use tensorlogic_ir::{TLExpr, Term};

// ¬(A ∧ B) becomes (¬A ∨ ¬B)
let a = TLExpr::pred("A", vec![]);
let b = TLExpr::pred("B", vec![]);
let expr = TLExpr::negate(TLExpr::and(a.clone(), b.clone()));
let nnf = tensorlogic_ir::to_nnf(&expr);
// Result: OR(NOT(A), NOT(B))