theonlineoasis

Compsci – Logic and proof

Propositional Logic

An intepretation is a function from the set of propositional symbols to $\{t,f\}$ . Tautologies (valid formulae) are satisfied (i.e. evaluate to true) under all interpretations. A set of statements is consistent is some interpretation satisfies all its elements at the same time. Otherwise, it is inconsistent. Satisfiable means the same as consistent, and unsatisfiable means the same as inconsistent.

A set $S$ of statements entails $A$ if every interpretation that satisfies S also satisfies A. We write $S \models A$ .

A canonical form for formulae in the propositional logic is Ordered Binary Decision Diagrams.

Ordered Binary Decision Diagrams

Note: in exams always write OBDD not BDD. Also, expand primitive connectives too, e.g. write out P and Q and combine to make $P \and Q$

Algorithm

Start at a node in each tree. Traverse the tree.
For identical nodes, map the require combining operator onto the subtrees.
For non-identical nodes, stay on the later node and work down the earlier one, add it to the result.
At leaf nodes, combine using the combining operator.

Official steps:

Recursively convert A and A' into BDDs Z and Z'.
Check for trivial cases (equal, t, f).
- Let Z = x P y, Z' = x' P' y'
- If same variable, build BDD recursively for (x op x') P (y op y')
- If P less than P', build BDD recursively for (x op z') P (y op z')
- If P greater than P', build BDD recursively for (z op x') P (z op y')

Optimization

We don't actually need subtree comparison -- leaf comparison will do. We can use pointer comparison.
Use hash tables.

Use an equivalence symbol to denote re-writing of trees.

Construction

Don't construct the entire tree.
Don't eliminate $\rightarrow$ , $\leftrightarrow$ , $\oplus$ or other connectives.
Tree $\lnot z$ as $z \rightarrow f$ or $z \oplus t$
Recursively convert operands.
Combine with ordering and sharing.
Remove redundant ones.
Test in order.
Each variable can over ever appear once.

Ordering

A bad ordering can lead to exponential length diagram.
If we have $P_1 < \ldots < P_n < Q_1 < \ldots < Q_n$ , the Conjunctive Normal Form expression $(P_1 \and Q_1) \or (P_2 \and Q_2) \or (P_3 \and Q_3) \ldots$

First order logic

Compared to Propositional Logic

Similar to propositional logic, but now instead of just $\{t, f\}$ we have some 'things'. We have predicates which map from things to $\{t, f\}$ and functions which map from 'things' to 'things'.

Definitions

Terms stand for individuals.

Formulae stand for truth values.

Variables $\{x, y, \ldots\}$ range over individuals.

A first-order language contains a set of $n$ -place function symbols and $n$ -place predicate symbols.

Constant symbols $\{a, b, \ldots\}$ are $0$ -place function symbols. Intuitively, they are names for fixed elements of the universe. Two constants may have the same meaning. It is not required to have a constant for each element.

Predicate symbols are also called relation symbols.

The terms of a first-order language are defined recursively as follows:

A variable is a term.
A constant symbol is a term.
If $t_1, \ldots, t_n$ are terms and $f$ is an $n$ -place function symbol then $f(t_1, \ldots, t_n)$ is a term.

The formulae of a first-order language are defined recursively as follows:

If $t_1, \ldots, t_n$ are terms and $P$ is an $n$ -place function symbol then $P(t_1, \ldots, t_n)$ is a formula (called an atomic formula).
If $A$ and $B$ are formulae then $\lnot A, A \and B, A \or B, A \rightarrow B, A \leftrightarrow B$ are also formulae.
If $x$ is a variable and $A$ is a formula then $\forall x A$ and $\exists x A$ are also formulae.

An interpretation of a language maps its function symbols to actual functions and its relation symbols to actual relations.

Let $\mathcal{L}$ be a first-order language. The interpretation $\mathcal{I}$ of $\mathcal{L}$ is a pair $(D, I)$ , $D$ being a non-empty set, the domain or universe.

if $c$ is a constant symbol (of $\mathcal{L}$ ), then $I[c] \in D$
if $f$ is an $n$ -place function symbol then $I[f] \in D^n \to D$ .
if $P$ is an $n$ -place relation symbol then $I[P] \subseteq D^n$ .

A valuation $V$ of $\mathcal{L}$ over $D$ is a function from the variables of $\mathcal{L}$ into $D$ . Write $\mathcal{I}_V[t]$ for the value of $t$ with respect to $\mathcal{I}$ and $V$ , defined by:

$\mathcal{I}_V[x]$ is defined as $V(x)$ where $x$ is a variable.
$\mathcal{I}_V[c]$ is defined as $I[c]$
$\mathcal{I}_V[f(t_1, ..., t_n)]$ is defined as $I[f](\mathcal{I}_V[t_1], \ldots, \mathcal{I}_V[t_n])$

Write $V\{a/x\}$ for the valuation that maps $x$ to $a$ and it otherwise the same as $V$ .

Reducing first order logic to propositional logic

Prenex Normal Form

$\lnot (\forall x A) \simeq \exists x \lnot A$

$\lnot (\exists x A) \simeq \forall x \lnot A$

Assuming there are no $x$ s in $B$ , we have:

$(\forall x A) \and B \simeq \forall x (A \and B)$

$(\forall x A) \or B \simeq \forall x (A \or B)$

Skolemization

To reduce $\forall x_1 \forall x_2 \ldots \forall x_k \exists y A$ (can have $k = 0$ ):

Take the leftmost $\exists y$ , delete this and replace $y$ in the expression with $f(x_1, x_2, \ldots, x_k)$ .

$\forall x_1 \forall x_2 \ldots \forall x_k A[f(x_1, x_2, \ldots, x_k) / y]$

Repeat until no more $\exists$ remain.

Example:

$\exists x [P(x) \rightarrow \forall y P(y)]$

Negated goal $\lnot [\exists x[P(x) \rightarrow \forall y P(y)]]$

NNF $\forall [P(x) \and \exists y \lnot P(y)]$

Pull $\exists$ out $\forall x \exists x [P(x) \and \lnot P(y)$

Skolemize $f(x)$ $\forall x [P(x) \and \lnot P(f(y))]$

Final clauses: $\{P(x)\}, \{\lnot P(f(x))\}$

Herbrand seminatics

Terms

This represents the syntax of formulae. That is, $X + 0$ cannot be $0$ .

Predicates

$P$ simply stands for the set of ground atoms $P(x)$ that we want to be true.

For example, the clauses $\lnot \mathrm{even}(1)$ , $\mathrm{even}(2)$ and $\mathrm{even}(X \cdot Y) \leftarrow \mathrm{even}(X), \mathrm{even}(Y)$ . For this, the Herbrand universe $\mathbb{H} = \{1, 2, 1 \cdot 1, 1 \cdot 2, 2 \cdot 1, 2 \cdot 2, 1 \cdot (1 \cdot 1)\}$ . $I[\mathrm{even}] = \{ \mathrm{even}(2), \mathrm{even}(1 \cdot 2) \}$ .

We can only vary the meaning of predicates. Therefore we can make any system. For example, this system works for $\cdot$ stands for $+$ , where we change the meaning of $\mathrm{even}$ .