Type the implication-as-disjunction law (used to convert to clause form)

Answer

P -> Q == not P or Q

Rewriting P → Q as ¬P ∨ Q is the first step in converting toward conjunctive normal form for resolution. You will use it again in Lesson 7 and in Module 9.