Two formulas \(F\) and \(G\) are said to be equivalent, written \(F \equiv G\), if they have the same truth value under every interpretation. In other words, for every interpretation \(I\), \(I \models F\) if and only if \(I \models G\).

1. \(\bot \equiv \bot \)
2. \(\top \equiv \top \)
3. \(\neg \top \equiv \neg \bot \)
4. \(\neg (p \land q) \equiv \neg p \lor \neg q\)
5. \(p \equiv p \lor q\)
6. \(\neg \neg p \equiv p\)

A formula \(F\) is in Negation Normal Form (NNF) if the negation operator \(\neg \) is only applied to literals (i.e., propositional variables or their negations), and the only other allowed operators are conjunction \(\land \) and disjunction \(\lor \). A nice way to think about it is that we can never have the case where we need to apply De Morgan's laws to push negations further down the formula tree. So all negations come pre-distributed to the literals.

1. \(p \to q\)
2. \(p \lor (\neg q \land (r \lor \neg s))\)
3. \(p \lor (\neg q \land \neg (\neg r \land s))\)
4. \(p \lor (\neg q \land (\neg \neg r \lor \neg s)) \)

The distributive law of conjunction over disjunction states that for any formulas \(F\), \(G\), and \(H\), the following equivalence holds:

To eliminate implications (\(\to \)) and biconditionals (\(\leftrightarrow \)) from a formula \(F\), we can use the following equivalences:

A formula \(F\) is in Disjunctive Normal Form (DNF) if it is a disjunction of one or more conjunctions of one or more literals. In other words, \(F\) can be expressed as a series of clauses connected by disjunctions (\(\lor \)), where each clause is a series of literals connected by conjunctions (\(\land \)). A literal is either a propositional variable or its negation.

Where each clause \(C_i\) is of the form:

Convert the following formula into Disjunctive Normal Form (DNF):

Two formulas are said to be equisatisfiable if either both formulas are satisfiable or both are unsatisfiable. In other words, there exists an assignment of truth values to the variables that makes one formula true if and only if there exists; not necessarily the same assignment; that makes the other formula true. Equisatisfiability is a weaker condition than logical equivalence, as equisatisfiable formulas may not have the same truth values under all assignments, but they share the same satisfiability status.

If a formula \(F\) and \(G\) are equisatisfiable, then are they equivalent?

A formula is in Conjunctive Normal Form (CNF) if it is expressed as a conjunction of disjunctions of literals. In other words, a CNF formula is a series of clauses (disjunctions) connected by AND operators. Each clause contains literals (variables or their negations) connected by OR operators. For example, the formula \((p \lor \neg q) \land (r \lor s \lor \neg t)\) is in CNF.

Where each clause \(C_i\) is of the form:

When converting a formula to Disjunctive Normal Form (DNF) or Conjunctive Normal Form (CNF), the size of the resulting formula can grow exponentially in the worst case. This is known as the exponential blow up problem. For example, a formula with \(n\) variables can result in a DNF or CNF with up to \(2^n\) clauses.

Tseytin's transformation is a method used in propositional logic to convert any given formula into an equisatisfiable formula in Conjunctive Normal Form (CNF). The key idea behind Tseytin's transformation is to introduce new variables to represent subformulas of the original formula, thereby avoiding an exponential increase in size that can occur with naive CNF conversion methods. There are two key properties of Tseytin's for a formula \(F\) and its Tseytin transformation \(F'\):

1. unsatisfiability: \(F\) is unsatisfiable if and only if \(F'\) is unsatisfiable.
2. model correspondence: For every satisfying assignment (model) of \(F'\), there exists a corresponding satisfying assignment of \(F\), and vice versa, when restricted to the original variables of \(F\).

To demonstrate how it works lets consider the following formula

1. Subformula identification: Identify the subformulas of \(\phi \) and assign a new variable to each subformula. For our example, we can identify the following subformulas and assign new variables: \[ \begin {align*} & \neg s \\ & p \lor q \\ & (p \lor q) \land r \\ & ((p \lor q) \land r) \to (\neg s) \end {align*} \]
2. Variable assignment: Assign new variables to each subformula: \[ \begin {align*} & x_1 \text { for } \neg s \\ & x_2 \text { for } p \lor q \\ & x_3 \text { for } (p \lor q) \land r \\ & x_4 \text { for } ((p \lor q) \land r) \to (\neg s) \end {align*} \]
3. Equivalence clauses: For each subformula, create clauses that enforce the equivalence between the new variable and the subformula it represents. For our example, we would create the following clauses: \[ \begin {align*} & (x_1 \leftrightarrow \neg s) \\ & (x_2 \leftrightarrow (p \lor q)) \\ & (x_3 \leftrightarrow (x_2 \land r)) \\ & (x_4 \leftrightarrow (x_3 \to x_1)) \end {align*} \]
4. Conjunct of clauses: Combine all the equivalence clauses into a single formula in CNF. The final formula \(\phi '\) will be the conjunction of all these clauses along with the clause that asserts the truth of the variable representing the entire formula (in this case, \(x_4\)): \[ \phi ' = (x_1 \leftrightarrow \neg s) \land (x_2 \leftrightarrow (p \lor q)) \land (x_3 \leftrightarrow (x_2 \land r)) \land (x_4 \leftrightarrow (x_3 \to x_1)) \land x_4 \]
5. Conversion to CNF: Finally, convert the combined formula into CNF using standard techniques (like distributing disjunctions over conjunctions). The resulting formula will be in CNF and equisatisfiable to the original formula \(\phi \). For example if we consider the clause \[ x_2 \leftrightarrow (p \lor q) \] this can be converted to CNF as \[ (x_2 \lor \neg p) \land (x_2 \lor \neg q) \land (\neg x_2 \lor p \lor q) \]

Lets consider the following formula

Using Tseytin's transformation, convert the formula \(F\) into an equisatisfiable formula in CNF.