Use Tseytin transformation to find $T(\phi):$ $$\phi\equiv¬(((P → Q) ∧ (Q → R)) → (P → R))$$

I did find an example on wiki for Tseytin transformation, and try to follow it to solve this, but not sure if this is right. Here is my attempts:

Consider $\phi$ as following, that have six subformulas:

$$\underbrace{¬\underbrace{(\underbrace{(\underbrace{(P → Q)}_{A} ∧ \underbrace{(Q → R)}_{B})}_{D} → \underbrace{(P → R)}_{C})}_{E}}_{F}$$

That $T(\phi)$ have seven clauses:

\begin{align} &A\leftrightarrow P → Q\\ \land&B\leftrightarrow Q → R\\ \land&C\leftrightarrow P → R\\ \land&D\leftrightarrow A\land B\\ \land&E\leftrightarrow D\to C\\ \land&F\leftrightarrow \neg E\\ \land&F\\ \end{align}

Transform each clause into CNF we have:

\begin{align} &(\neg P\lor Q\lor\neg A)\land(P\lor A)\land(\neg Q\lor A)\\ \land&(\neg Q\lor R\lor\neg B)\land(Q\lor B)\land(\neg R\lor B)\\ \land&(\neg P\lor R\lor\neg C)\land(P\lor C)\land(\neg R\lor C)\\ \land&(\neg A\lor\neg B\lor D)\land(A\lor\neg D)\land(B\lor\neg D)\\ \land&(\neg D\lor C\lor\neg E)\land(D\lor E)\land(\neg C\lor E)\\ \land&(E\lor\neg F)\land(\neg E\lor F)\\ \land&F\\ \end{align}

Could someone verify this, Thanks for your help.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.