Thanks a lot already in advance for any help!
In short, I am in need somewhat like a syntactic proof that the disjunction of two unsatisfiable propositional formulas is unsatisfiable.
More precisely, assume that we given a propositional formula $\Phi$ in CNF. We write each clause $\bar p_{1} \vee \dots \vee \bar p_{m} \vee q_{i} \vee \dots \vee q_{l}$ as an implication of the form $\bigwedge_{i=1}^m p_{i} \rightarrow \bigvee_{j=1}^l q_j$. Hence, $\Phi$ can be written as $$ \Phi = \bigwedge_{c=1}^n \bigwedge_{i=1}^{m_c} p_{c,i} \rightarrow \bigvee_{j=1}^{l_c} q_{c,j}. $$
An empty conjunction $\bigwedge_{i=1}^{m_c} p_{c,i}$ translates into the truth constant True, i.e. $\bigwedge_{i=1}^0 p_{c,i} = \top$, and analogously $\bigvee_{j=1}^0 q_{c,j} = \bot$.
Now, consider the following algorithm to test whether such a propositional formula $\Phi$ is unsatisfiable:
Input: propositional formula $\Phi$ in CNF
Output: SAT if $\Phi$ is satisfiable, UNSAT otherwise$M \leftarrow \{\{\top\}\}$
do
$\quad M \leftarrow \bigcup_{N \in M} \{N \cup \{q_{c_1,j_1},\dots,q_{c_k,j_k} \} \; \mid 1 \leq c_1 < c_2 < \dots < c_k \leq n,$
$\hspace{15.4em} 1 \leq j_\alpha \leq l_{c_\alpha},$
$\hspace{15.4em}$ if $l_{c_\alpha} = 0$, then $q_{c_\alpha,j_\alpha} := \bot$,
$\hspace{15.4em} p_{c_\alpha,i} \in N$ for all $i = 1,\dots,m_{c_\alpha} \} $
while M has changedif $\bot \in \bigcap_{N \in M} N$
$\quad$ return UNSAT
else
$\quad$ return SAT
Essentially the algorithm iteratively builds all possible models of $\Phi$ (each set $N$ in $M$ corresponds to one candidate model) by adding to a set $N$ all combinations of right hand sides of those implications for which the left hand sides are contained in $N$. It marks all ''failed'' models, i.e. all sets $N$ that contain a contradiction by $\bot$. If finally all candidates contain a contradiction, $\Phi$ must be unsatisfiable. Otherwise $\Phi$ is satisfiable.
I think the workings of the algorithm become most clear by considering an example. Let $\Phi = (\top \rightarrow a \vee b) \wedge (a \rightarrow \bot) \wedge (b \rightarrow d) \wedge (d \rightarrow \bot)$.
Then the set $M$ evolves as follows:
$M_0 = \{\{\top\}\}$
$M_1 = \{\{\top,a\}, \{\top,b\}\}$
$M_2 = \{\{\top,a,\bot\},\{\top,a,b,\bot\},\{\top,b,a,d\},\{\top,b,d\}\}$
$M_3 = \{\{\top,a,\bot\},\{\top,a,b,\bot\},\{\top,b,a,d,\bot\},\{\top,b,d,\bot\}\}$
Since all sets in $M$ contain $\bot$, $\Phi$ is unsatisfiable.
Now I want to show that if the algorithm returns UNSAT for $\Phi_1$ and $\Phi_2$ (given separately as input), then it also returns UNSAT for $\Phi_1 \vee \Phi_2$.
My goal was to find some invariant that allows me to relate the sets $M_n$ that are formed during the $n$-th iteration of the while-loop when given $\Phi_1$ and $\Phi_2$ as input to the sets in $M_n$ when given $\Phi_1 \vee \Phi_2$ as input. But so far I could not find anything useful.
Any suggestions are very much appreciated!