The notation for NAND and NOR can be thought of as \(\land, \lor\) with vertical bars through the middle of them - i.e. \(\uparrow, \downarrow\).

The notation for XNOR and XOR respectively are \(\equiv\) and \(\not \equiv\) (think about the truth tables.)

I use \(\implies\) with the double arrow, the exam uses \(\rightarrow\) the single arrow. Please bear in mind.

Top \(\top\) and bottom \(\bot\) are True and False respectively.

The degree of a parse tree is the number of inner nodes.

A valuation is "a mapping of a formula to true or false" i.e. what it resolves to. Always true: tautology. Always false: contradiction. Sometimes true: satisfiable.

X is a consequence of S (set) \(S \models X\) if every formula in S is true \(\implies\) X is true. A tautology is a consequence of nothing \(\models X\).

Write a conjunction \(X_1 \land X_2 \land \cdots\) as an angle list \(\langle X_1, X_2, \cdots \rangle\) and a disjunction \(Y_1 \lor Y_2 \lor \cdots\) as a square list \([Y_1, Y_2, \cdots]\). X can be a complex formula, or a literal (\(\top, \bot, x, \lnot x\)). A disjunction of literals is a clause and it's conjunction counterpart is a dual clause.

The conjunctive normal form is a conjunction of disjunctions \(\langle [] \rangle\) of literals. And is associated with alpha \(\alpha\).

The disjunctive normal form is a disjunction of conjunctions \([ \langle \rangle ] \) of literals. Or is associated with beta \(\beta\).

Every binary formula under the sun (except xor and xnor) can be reduced to \(A \land B\) or \(A \lor B\), where \(A, B\) can be literals or other formulas, via a combination of simplifying formulas like \(\implies\) and de-morgan's law.

Note \(A \nRightarrow A \equiv \lnot (A \Rightarrow A) \equiv \lnot (\lnot A \lor A) \equiv A \land \lnot A.\)

If a formula simplifies to \(A \land B\), it is an alpha formula. If it simplifies to \(A \lor B\), it is a beta formula.

Reduction to CNF

From a truth table, look at rows with False as output. Write the "inverse or", i.e. if a row is \(x=T, y=T, z=F \longrightarrow F\), then the clause for that row is \([\lnot x, \lnot y, z] \). Put all of these clauses together in a conjunction.

For a formula \(X\), start by writing \(\langle [X] \rangle\), then reduce via algorithm.

In short, the algorithm is represented as: \[ \begin{array} {|r|r|}\hline \lnot \top & & \lnot \bot & & \lnot \lnot Z & & \beta & & \alpha & \\ \hline \bot & & \top & & Z & & \beta_1 & & \alpha_1 & \alpha_2 \\ \hline & & & & & & \beta_2 & & & \\ \hline \end{array} \] Where \(\beta\) is a beta formula (\(\beta_1 \lor \beta_2\)), and \(\alpha\) is an alpha formula (\(\alpha_1 \land \alpha_2\)).
In long:

• If beta: \(\langle \cdots [\beta_1 \lor \beta_2, \cdots] \cdots \rangle\), replace the \(\lor\) with a comma.
• If alpha: \(\langle \cdots [\alpha_1 \land \alpha_2, \cdots] \cdots \rangle\), copy the disjunction it's in, and in the place of \(\alpha_1 \land \alpha_2\) put \(\alpha_1\) in one and \(\alpha_2\) in the other.
• Otherwise replace in place as shown.

Repeat until all items are literals.

Reduction to DNF

From a truth table, look at the rows with True as output. Write the and of the literals, i.e. if a row is \(x=T, y=F, z=T \longrightarrow T\), write the dual clause \(\langle x, \lnot y, x \rangle\). Put all of these together in a disjunction.

For a formula start with \([\langle X \rangle] \). The algorithm is identical, except the role of the \(\alpha\) and \(\beta\) is swapped. \[ \begin{array} {|r|r|}\hline \lnot \top & & \lnot \bot & & \lnot \lnot Z & & \beta & & & \alpha \\ \hline \bot & & \top & & Z & & \beta_1 & \beta_2 & & \alpha_1 \\ \hline & & & & & & & & & \alpha_2 \\ \hline \end{array} \]

Two methods, semantic tableau (tree) ~ DNF, and resolution ~ CNF.

Both prove if a formula is a tautology by contradiction.

Semantic Tableau

Tree form. Branches (from root to tip) are conjunctions (ands), and the whole tree's "value" is a disjunction (ors) of branches. We prove by expanding branches. A node can be expanded multiple times, but in a strict tableau expand only once, but this is still sufficient.

To prove a formula \(X\), start with the antiformula \(\lnot X\) as the root of the tree. Now look at the DNF table.

1. If there is an alpha formula, add two nodes to the end of any branch it is on with those \(\alpha_1, \alpha_2\) values (like in table).
2. If there is a beta formula, add a split onto the end of that branch, and make two new branches from it with the \(\beta_1, \beta_2\).
3. Close a branch if that branch, somewhere along it, has a formula \(X\), and its antiformula \(\lnot X\). This is an atomic closure if X, ¬X are atomic.

When all branches are closed, X is proved to be a tautology. Denote a tableau proof as \(\vdash_t X\).

Resolution

The dual to the tableau, this one is just written as a numbered list of disjunctions. Similarly it proves X is a tautology by contradiction.

Make line 1 \([\lnot X] \). Then look at the CNF table

1. If there is a beta forumla, replace that formula with \(\beta_1, \beta_2\) (comma). (Write the updated thing on a new line)
2. If there is an alpha formula, copy that line onto two new lines, one with the \(\alpha_1\), one with the \(\alpha_2\).
3. If one line has a formula X, and the other line has a formula ¬X, perform the resolution rule: make a new line with all the formulas from the prior two except any Xs and ¬Xs. Do not try do this over multiple different formulas in one go.

When [] is found then the resolution is considered proved. Denote as \(\vdash_r X\). A line can be "expanded" multiple times, and we also have the idea of "strictness" in resolution.

Proving Consequence

To prove \(S \models X\) (for a set S of formulas), add an S-introduction rule to both methods.

• Tableau: Add any formula from S onto the end of any branch at any time.
• Resolution: Add any formula from S as a new line at any time.

Denote these proofs as \(S \vdash_t X\) and \(S \vdash_r X\).

Natural Deduction

Note: all boxes here are done horizontally for easy formatting. They should be vertical in reality.

Two techniques to prove a formula: start with the antiformula, or work backwards (e.g. for \(x \implies y\) we must assume \(x\) and logically conclude \(y\)).

In proving only active formulas not in closed boxes can be used.

Assumptions and Premises

Assumptions start a box: \([x \cdots\). Premises are formulas S-introduced when proving consequence, and do not start a box.

Standard Rules

A double arrow is used for implies, a single arrow is used for "produces"

• Constant rule: \(\bot \longrightarrow X\) (from false can introduce any X)
• Constant rule: \(\longrightarrow \top\) (anthing can introduce true)
• Negation rule: \(X, \lnot X \longrightarrow \bot\)
• Negation rule: \([X \cdots \bot] \lnot X\) or \([\lnot X \cdots \bot] X\)
• Alpha elim: \(\alpha \longrightarrow \alpha_1\) or \(\alpha \longrightarrow \alpha_2\)
• Alpha introduction: \(\alpha_1, \alpha_2 \longrightarrow \alpha\)
• Beta elim: \(\lnot \beta_1, \beta \longrightarrow \beta_2\) or \(\lnot \beta_2, \beta \longrightarrow \beta_1\)
• Beta introduction: \([\lnot \beta_1 \cdots \beta] \beta_2\) or \([\lnot \beta_2 \cdots \beta] \beta_1\)

Derived rules

• Double negation: \(\lnot \lnot X \longrightarrow X\) or \(X \longrightarrow \lnot \lnot X\)
• Copy: \(X \longrightarrow X\)
• Implication: \([X \cdots Y] (X \implies Y)\)
• Excluded middle: \(\top \longrightarrow X \lor \lnot X\)
• Modus ponens: \(X, X \implies Y \longrightarrow Y\)
• Modus tollens: \(\lnot Y, X \implies Y \longrightarrow \lnot X\)

Write as \(S \vdash_d X\) if S entails X has a deduction proof.