Quantifiers: Atomic Tableaux AFavp(v)+ for some ground term t, AFp(t) 7(彐x)y( T( for a new constant cQuantifiers: Atomic Tableaux A |= ∃vϕ(v ) ⇔ for some ground term t, A |= ϕ(t). T(∃x)ϕ(x) Tϕ(c) for a new constant c Yi Li (Fudan University) Discrete Mathematics June 5, 2012 6 / 25