I am trying to proof by resolution the following:
1) Given a language with the binary relation symbols $<, <<, <<<$ and the binary function symbols $+, *$ and the constant symbols a, b,
proof by resolution that the following CNF is unsatisfiable:
$\{\{a+b < a*b\}; \{x_2 \not< y_2, x_2 + y_2 << x_2 * y_2\}; \{x_2 \not<< y_2, x_2 + y_2 <<< x_2 * y_2\}; \{x \not<<< y\}\}$
Hint: Find a set of instances without free variables of this clauses, that are propositionally unsatisfiable.
I don't manage to find suitable instances of the clauses. Do you have any idea?
2) Name a set of n clauses (with O(n) symbols) that is unsatisfiable, but whereby the smallest set of instances without free variables, that are propositionally unsatisfiable, does have more than O(n) symbols.
I have no idea how such a set of clauses could look like. Hopefully it becomes more clear, when 1) is solved?
I'd appreciate your help on this! :)
You need to use $a+b < a*b$ in some other clause. The operator "$<$" only occurs in $x_2 \not< y_2$ so you should take $x_2=a+b, y_2=a*b$. The other instantiations follow the same reasoning. So you end up with clauses,
\begin{align*} & a+b < a*b\\\\ & a+b \not< a*b\\ & (a+b) + (a*b) \ll (a+b) * (a*b)\\\\ & (a+b) + (a*b) \not\ll (a+b) * (a*b)\\ & ((a+b)+(a*b))+((a+b)*(a*b)) \lll ((a+b)+(a*b))*((a+b)*(a*b))\\\\ & ((a+b)+(a*b))+((a+b)*(a*b)) \not\lll ((a+b)+(a*b))*((a+b)*(a*b))\\\\ \end{align*}
Applying the resolution method is now trivial.
For question number 2 consider,
\begin{align*} &\{a+b <_1 a*b\}\\ % &\{x_k \not<_{(k-1)} y_k,\ x_k + y_k <_k x_k * y_k\}\quad 1<k<n\\ &\{x_{n} \not<_{n-1}< y_{n}\} \end{align*}
and to instantiate the free variables consider terms, $s_0 = a$, $t_0 = b$, $s_k =s_{(k-1)}+t_{(k-1)}$ and $t_k =s_{(k-1)}*t_{(k-1)}$, and define substitutions $x_k/s_{k-1}$ and $y_k/t_{k-1}$ for $1<k<n$. The number of symbols grows exponentially with $k$ and therefore also with $n$.