--- Resolution --- Ax (a(x)&-s(x) <-> -p(x)) C1 = {s(x1), -a(x1), -p(x1)} C2 = {p(x2), -s(x2)} C3 = {p(x3), a(x3)} 1) C4 = {a(c)} C5 = {s(d)} C6 = {p(e)} (negation of thesis) Derived clauses: C7 = {s(c), -p(c)} (C1+C4) C8 = {p(d)} (C2+C5) C9 = {s(d), -a(d)} (C1+C5) C10 = {-p(c), p(c)} (C2+C7) (this is a tautological clause, and therefore useless) C11 = {-s(c), s(c)} (C2+C7) (this is a tautological clause, and therefore useless) C12 = {s(c), a(c)} (C3+C7) C13 = {s(e),~a(e)} (C6+C1) C14 = {p(d), -a(d)} (C2+C9) C15 = {p(d), s(d)} (C3+C9) C17 = {a(c),p(c)} (C12+C2) C18 = {a(c),s(c),~a(c)} (C17+C1) (this is a tautological clause, and therefore useless) C19 = {p(e),~a(e)} (C13+C2) C20 = {p(e),s(e)} (C13+C3) C22 = {p(c),s(c),~p(c)} (C17+C1) (this is a tautological clause, and therefore useless) C22 = {a(x4),s(x4),~a(x4)} (C1+C3) (this is a tautological clause, and therefore useless) C23 = {p(x5),s(x5),~p(x5)} (C1+C3) (this is a tautological clause, and therefore useless) C24 = {p(x6),~a(x6),~p(x6)} (C1+C2) (this is a tautological clause, and therefore useless) C25 = {s(x7),~a(x7),~s(x7)} (C1+C2) (this is a tautological clause, and therefore useless) All other derivable clauses are either (variants of) already derived clauses or involve tautological clauses, that are useless for the derivation of the empty clause. Therefore the argument is not valid! 2) C4 = {a(c)} C5 = {s(d)} C6 = {-p(x)} (negation of thesis) Derived clauses: C7 = {p(d)} (C2+C5) C8 = {} (C7+C6) Valid! 3) C4 = {a(c)} C5 = {s(x)} C6 = {-p(e)} Derived clauses: C7 = {-s(e)} (C2+C6) C8 = {} (C7+C5) Valid! --- Tableaux -- 1) Ax (f(x)&-c(x)->t(x)) = Ax (t(x)|c(x)|-f(x)) f(a) (apple is a fruit) -c(a) -t(a) (negation of thesis) 3 branches, all closed 2) Ax (-l(d,x)|l(x,m)) & Ax (l(d,x)|-l(x,m)) Ax (l(m,x)|l(x,d)) & Ax (-l(m,x)|-l(x,d)) l(d,d) -l(m,m) (negation of thesis) (up to) 16 branches, all closed --- Natural deduction --- 1 Ex(F->G) 2 F[x/a]->G (existential elimination) (note that G[x/a]=G since x does not occur free in G) 3 . AxF (assumption) 4 . F[x/a] (universal elimination) 5 . G (modus ponens 5+2) (AxF)->G (implication introduction 3+6)