The question concerns the resolution proof in the propositional logic. Always active: for all and is valid: ( ∨ ) ∧ (′ ∨ ¬) ≡ ( ∨ ) ∧ (′ ∨ ¬) ∧ ( ∨ ′)
now the proof gets extended with (φ∨u∨¬v)∧(ψ∨¬u∨v) ≡ (φ∨u∨¬v)∧(ψ∨¬u∨v)∧(φ∨ψ)
now the proof gets extended with (φ∨u) ≡ (φ∨u)∧(φ∨¬u)
now the proof gets extended with (φ∨u)∧(ψ∨¬u)∧(χ∨u∨¬u) ≡ (φ∨u)∧(ψ∨¬u)∧(χ∨u∨¬u)∧(φ∨ψ∨χ)
only one extension is active at a time. How do I show the soundness and completeness for each of the extended systems?