Resolution Proof

A resolution proof is a formula in a strict syntax, where sequences of certain formulae (called conclusions) must follow after other formulae (called premises) by rules of inference. A resolution proof requires a deductive system to provide these rules of inference.

Definition §

Resolution Proof ^definition

Let $P_1\dots P_n$ be well-formed formulae (wff) under some formal language, $L$. A resolution proof of a conclusion (which is also a wff), $C_m$ from some premises $P_1\dots P_n$ is a logical formula of the form:

$$P_1\dots P_n⊢C_1,C_2\dots C_m$$

where each $C_i$ is either:

• A copy of some $P_j$ OR
• A wff created by a rule of inference in a deductive system involving any 2 preceding wffs (either $P_j$ or a previous $C_k,k<i$)

If such a resolution proof exists from $P_{1\dots n}$ to $C_m$, then we write $P_1\dots P_n{⊢}_R{C}_m$

Resolution Proof (Propositional Logic) ^definition-propositional

Let $P_1\dots P_n$ be well-formed propositions in propositional logic A resolution proof of a conclusion (which is also a wff), $C_m$ from some premises $P_1\dots P_n$ is a logical formula of the form:

$$P_1\dots P_n⊢C_1,C_2\dots C_m$$

where each $C_i$ is either:

• A copy of some $P_j$ OR
• A wff created by the resolution rule involving any 2 preceding wffs (either $P_j$ or a previous $C_k,k<i$)

The definitions above are written in sequent notation, but could just as easily be written horizontally line-by-line (I don’t know what notation this is called):

$$P_1,P_2⊢C_1\text{ is the same as }\begin{array}{r}{P}_1\\ P_2\\ \therefore C_1\end{array}$$

Theorems §

T1: A resolution proof is sufficient to show semantic consequence (i.e. it is sound)

Take an arbitrary well-formed formula $C$ and a set of well-formed formulae $P_{\Sigma }=\{P_1,P_2,P_3,\dots \}$, both under the same logic, $L$. Then:

$$\text{If }{P}_{\Sigma }{⊢}_{R}C,\text{ then }(P_1\wedge P_2\wedge P_3\dots )\models C$$

$$P_{\Sigma }{⊢}_{R}C⟹(P_1\wedge P_2\wedge P_3\dots )\models C$$

• Here, ${⊢}_R$ means a resolution proof exists from $P_{\Sigma }$ that deduces $C$.
• $(P_1\wedge P_2\wedge P_3\dots )\models C$ : $C$ is a semantic consequence of $P_1\wedge P_2\dots$
• $⟹$ is a meta-implication, meaning it is not the same as $\to$ material implication used specifically in propositional logic

Meta-Proof:

#todo

The beauty of the theorem is that if we have a formal language, and a deductive system, we can create proofs of things before we even assign meaning to them!!

To get a better idea of this, I’m going to create an absurd formal language and a (broken, but we won’t worry about it) deductive system.

Let the symbol set be $\Sigma =\{\&,\%,@,\#\}$ and our formal language be:

$$L=\{w:w\in \{\Sigma {\}}^2\}\text{ i.e. all words of length 2}$$

Then, a deductive system can be

• We can deduce $@@$ from $@\ast$ combined with $\ast @$, where $\ast$ being any symbol in $\Sigma$ except $@$

I can create a resolution proof:

$$\&@,@\#⊢@@$$

by using that deductive system.

Now, even though we have no idea what any of the symbols mean (i.e. we have not assigned semantics), by theorem 1, we know our proof applies on every model! For example, let’s say we’re talking about cellular automata, where $\&$ is a red cell, $\#$ is a blue cell, and $@$ means either dead cell (if it is not attached to a red or blue cell), or it means a connecting living cell is attacking this spot.

We know now that combining a ‘red cell attacking right’ with a ‘blue cell attacking left’ results in ‘both cells die’.

Examples §

Examples: Propositional Logic §

• $P\vee Q,\neg Q⊢P$ is a resolution proof, as the $P$ on the LHS of the $⊢$ can be deduced using the resolution rule
• $P⊢P$ is a (pretty useless) resolution proof as well, because the LHS $P$ is a copy of the RHS $P$
• $P,\neg P⊢\perp$ is also a resolution proof, and is an example of a refutation

Non-examples: Propositional Logic §

• $A\vee B\vee C,\neg B,\neg C⊢A$ is not a resolution proof, because the $A$ on the RHS cannot be deduced using only two formulae with the resolution rule
  • $A\vee B\vee C,\neg B,\neg C⊢A\vee C,A$ is the right way to write it.
• $P,Q⊢R$ is not a resolution proof, because $R$ is neither a copy of either $P$ or $Q$, nor can it be deduced using the resolution rule.