Home

Ackermanization

Eliminate uninterpreted functions — reduce QF_UF to quantifier-free equality (QF_EQ)

QF_UF → QF_EQ
Formula Input
Syntax: f(x)=y  g(a,b)!=c   operators: & | ! -> <->   functions: any lowercase name followed by (args)
Algorithm Flow
φ — Input
↓
F-apps & Fresh ki
↓
Replace → φ'
↓
Congruence Axioms
↓
Ack(φ) = Axioms → φ'
↓
SAT Check
Ackermanization Trace
φ (original) —
F-applications —
φ' (replaced) —
Congruence axioms —
Ack(φ) —
Explanation

Enter a formula and click Run ▶ to start,
then step through the algorithm.