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.
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:
Repeat until all items are literals.
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.
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.
When all branches are closed, X is proved to be a tautology. Denote a tableau proof as \(\vdash_t X\).
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
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.
To prove \(S \models X\) (for a set S of formulas), add an S-introduction rule to both methods.
Denote these proofs as \(S \vdash_t X\) and \(S \vdash_r X\).
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 start a box: \([x \cdots\). Premises are formulas S-introduced when proving consequence, and do not start a box.
A double arrow is used for implies, a single arrow is used for "produces"
Write as \(S \vdash_d X\) if S entails X has a deduction proof.