ki1-zusammenfassung.tex

\documentclass{article}

\usepackage{geometry}
\geometry{a4paper, margin=0.5in, bottom=1in}

\usepackage[utf8]{inputenc}

\usepackage{amsfonts}
\usepackage{amsthm}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{stmaryrd}
\usepackage{bussproofs}
\usepackage{color}

\usepackage{multicol}
\setlength{\columnsep}{1cm}

\theoremstyle{definition}
\newtheorem{definition}{Definition}
\newtheorem{theorem}{Theorem}
\newtheorem{remark}{Remark}

\title{Artificial Intelligence I \\ Summary}
\author{Lorenz Gorse}

\begin{document}

\maketitle

\begin{center}
	\textcolor{red}{\uppercase{DISCLAIMER: This is not a complete summary. Errors are likely. The sole source are the lecture slides of the lecture "Künstliche Intelligenz I" of the winter term 16/17 at the Friedrich-Alexander University.}}
\end{center}

\begin{multicols*}{2}

\section{Agents}

\begin{definition}[Agent]
	An agent is an entity that perceives and acts. It is modeled as a function from percept histories to actions.
	$$\mathcal{P}^* \mapsto \mathcal{A}$$
\end{definition}

\begin{definition}[Performance measure]
	A performance measure is a function that evaluates a sequence of environments.
\end{definition}

\begin{definition}[Rationality]
	An agent is called rational, if it chooses the actions that maximizes the expected value of the performance measure given the percept history to date.
\end{definition}

\begin{definition}[Task environment]
	A combination of a performance measure, environment, actuators and sensors (PEAS) describes a task environment.
\end{definition}

\begin{definition}[Environment properties]
	For an agent $a$ we call an environment $e$
	\begin{description}
		\item[fully observable,] iff $a$'s sensors give it access to the complete state of $e$ at any point in time, else \textbf{partially observable}.
		\item[deterministic,] iff the next state of $e$ is completely determined by $a$'s action and $e$'s current state, else \textbf{stochastic}.
		\item[episodic,] iff $a$'s experience is divided into atomic, independent episodes, where it perceives and performs a single action. Non-episodic environments are called \textbf{sequential}.
		\item[dynamic,] iff $e$ can change without an action performed by $a$, else \textbf{static}.
		\item[discrete,] iff the sets of $e$'s states and $a$'s actions are countable, else \textbf{continuous}.
		\item[single-agent,] iff only $a$ acts on $e$.
	\end{description}
\end{definition}

\begin{definition}[Simple reflex agent]
	This is an agent that bases its next action only on the most recent percept.
	$$f_a: \mathcal{P} \mapsto \mathcal{A}$$
\end{definition}

\begin{definition}[Reflex agent with state]
	This is an agent with a FSM as a agent function. Inputs to the FSM are the percepts, outputs are a function of the current state and determine the actions.
\end{definition}

\begin{definition}[Goal-based agent]
\end{definition}

\begin{definition}[Utility-based agent]
	This is an agent that uses a world model along with a utility function that measures its preference among the states of the world. It chooses the action that leads to the best expected utility, which is computed by averaging over all possible outcome states, weighted by the probability of the outcome.
\end{definition}

\begin{definition}[Learning agent]
	This is an agent that augments the performance element (which chooses actions from percept sequences) with a
	\begin{description}
		\item[learning element] that makes improvements to the agent's performance element
		\item[critic] which gives feedback to the learning element based on an external performance standard
		\item[problem generator] which suggests actions that can lead to new, informative experiences
	\end{description}
\end{definition}

\section{Search}

\begin{definition}[Search problem]
	A search problem $$\mathcal{P} = \langle \mathcal{S}, \mathcal{O}, \mathcal{I}, \mathcal{G} \rangle$$ consists of a set $\mathcal{S}$ of states and a set $\mathcal{O} \subseteq \mathcal{S} \times \mathcal{S}$ of operators. Certain states in $\mathcal{S}$ are labeled as goal states $\mathcal{G} \subseteq \mathcal{S}$ and there is a single initial state $\mathcal{I} \in \mathcal{S}$. A cost function $c: \mathcal{O} \mapsto \mathbb{R}^+$ assigns costs to operators.
\end{definition}

\begin{definition}[Solution]
	A sequence of operators that lead from the initial state $\mathcal{I}$ to any goal state $g \in \mathcal{G}$ is a solution.
\end{definition}

\begin{definition}[Problem types]
	Problems come in many variations:
	\begin{description}
		\item[Single-state problem] ...
		\item[Multiple-state problem] ...
		\item[Contingency problem] ...
	\end{description}
\end{definition}

\begin{definition}[Tree search]
	This is an algorithm that explores state spaces according to a search strategy.
\end{definition}

\begin{definition}[Search strategy]
	A search strategy orders the nodes in the fringe. The following properties of search strategies are studied:
	\begin{description}
		\item[Completeness:] Does it always find a solution if one exists?
		\item[Time complexity:] Number of nodes generated/expanded.
		\item[Space complexity:] Maximum number of nodes held in memory.
		\item[Optimality:] Does it always find the least-cost solution?
	\end{description}
\end{definition}

\begin{definition}[Uninformed search]
	Search strategies that only employ information from the problem statement yield uninformed searches. Examples are breadth-first-search (BFS), uniform-cost-search (UCS), depth-first-search (DFS), depth-limited search, iterative-deepening-search (IDS).
\end{definition}

\begin{definition}[Informed search]
	Search strategies that use information about the real world beyond the problem statement yield informed searches. The additional information about the world is provided in form of heuristics. Examples are greedy-search and A*-search.
\end{definition}

\begin{definition}[Heuristic]
	A heuristic is an evaluation function $h: \mathcal{S} \mapsto \mathbb{R}^+ \cup \{\infty\}$ that estimates the cost from a state $n$ to the nearest goal state. If $n \in \mathcal{G}$, then $h(n)=0$.
\end{definition}

\begin{definition}[Goal distance function]
	The function $h^*: \mathcal{S} \mapsto \mathbb{R}^+ \cup \{\infty\}$ with $h^*(n)$ being the cost of the cheapest path from $n$ to a goal state is the goal distance function.
\end{definition}

\begin{definition}[Admissibility and consistency]
	A heuristic $h$ is admissible if $h(n) \leq h^*(n)$ for all states $n \in \mathcal{S}$. A heuristic $h$ is consistent if $h(s) - h(s') \leq c(o)$ for all $s \in \mathcal{S}$ and $o = (s, s') \in \mathcal{O}$.
\end{definition}

\begin{definition}[Greedy-search]
	Greedy-search always expands the node that seems closest to a goal state, as measured by the heuristic.
\end{definition}

\begin{definition}[$A^*$-search]
	$A^*$-search always expands the node that has the smallest sum of current path cost and estimated distance to the nearest goal state.
\end{definition}

\begin{definition}[Local search]
	A search algorithm that only operates on a single space at a time is called a local search. Local search algorithms need constant space. One example is hill-climbing: \begin{enumerate}
		\item Start with any state $n$.
		\item Move to the successor $n$ of the current state for which $h(n)$ is minimal.
	\end{enumerate}
\end{definition}

\begin{definition}[Game state space]
	A 6-tuple $\Theta = (S, A, T, I, S^T, u)$ is a game state space.
	\begin{itemize}
		\item $S$ are the states of the game. This is the disjoint union of $S^{Max}$ (When it's Max's move), $S^{Min}$ (When it's Min's move) and $S^T$ (When the game is over).
		\item $A$ are the possible moves. This is the disjoint union of $$A^{Max} \subseteq S^{Max} \times (S^{Min} \cup S^T)$$ and $$A^{Min} \subseteq S^{Min} \times (S^{Max} \cup S^T)$$
		\item $S^T$ is the set of terminal states.
		\item $u: S^T \mapsto R$ is the utility function. Each terminal state is assigned a value, which is interpreted as the score for Max (and the negative score for Min).
	\end{itemize}
\end{definition}

\begin{definition}[Game search]
	TODO: Minimax, Alpha-Beta-Pruning, MCTS
\end{definition}

\section{Constraint Satisfaction Problems}

\begin{definition}[Constraint Satisfaction Problem]
	Abbreviated as CSP. This is a search problem where the states are induced by a finite set $V = \{X_1, \dots, X_n\}$ of variables and domains $\{D_v | v \in V\}$ and the goal test is a set of constraints specifying allowable combinations of values for subsets of variables.

	A partial assignment is a partial function $a: V \mapsto \bigcup_{v \in V} D_v$ if $a(v) \in D_v$ for all $v \in V$. We call $a$ an assignment if $a$ is total.

	A partial assignment $a$ is inconsistent, iff there are variables $u, v \in V$ and a constraint $C_{uv} \in C$ and $(a(u), a(v)) \not\in C_{uv}$. $a$ is called consistent iff it is not inconsistent.

	A consistent assignment is called as solution.

	The states of the problem are the partial assignments, the initial state is the empty assignment, the goal states are the consistent assignments and the operators are partial assignment extensions.

	The CSP is called binary if all constraint relate at most two variables.
\end{definition}

\begin{definition}[Constraint network]
	A triple $\langle V, D, C \rangle$ is called a constraint network, where
	\begin{itemize}
		\item $V = \{X_1, \dots, X_n\}$ is a finite set of variables
		\item $D = \{D_v | v \in V\}$ the set of their domains
		\item $C = \{C_{uv} | u,v \in V\}$ a set of binary constraints. Each binary constraint is a symmetric relation $C_{uv} \subseteq D_u \times D_v$.
	\end{itemize}
\end{definition}

\begin{remark}
	Binary CSPs can be formulated as constraint networks.
\end{remark}

\begin{definition}[Minimum remaining values]
	This is a heuristic for backtracking searches on CSPs. It says: Assign the variable with the fewest remaining legal values next.
\end{definition}

\begin{definition}[Degree heuristic]
	This is a heuristic for backtracking searches on CSPs. It says: Assign the variable with the most constraints on remaining variables next.
\end{definition}

\begin{definition}[Least constraining value]
	This is a heuristic for backtracking searches on CSPs. It says: When assigning a variable, choose the value that rules out the fewest values from the neighboring domains.
\end{definition}

\begin{remark}
	A popular heuristic combines the three heuristics above: From the set of most constrained variables, pick the most constraining variable and assign the least constraining value.
\end{remark}

\begin{definition}[Equivalent constraint networks]
	Two constraint networks $\gamma = \langle V, D, C \rangle$ and $\gamma' = \langle V, D', C' \rangle$ are equivalent ($\gamma \equiv \gamma'$) iff they have the same solutions.
\end{definition}

\begin{definition}[Tightness]
	Let $\gamma = \langle V, D, C \rangle$ and $\gamma' = \langle V, D', C' \rangle$ be two constraint networks. $\gamma'$ is said to be tighter than $\gamma$ ($\gamma' \sqsubseteq \gamma$) iff
	\begin{itemize}
		\item For all $v \in V$: $D'_v \subseteq D_v$
		\item For all $u, v \in V$: $C_{uv} \notin C$ or $C'_{uv} \subseteq C_{uv}$
	\end{itemize}
\end{definition}

\begin{remark}
	An equivalent but tighter constraint network is preferable, because it has fewer consistent partial assignments.
\end{remark}

\begin{definition}[Forward checking]
	For a constraint network $\gamma$ and a partial assignment $a$, remove all values from the domains of unassigned variables that are in conflict with the values of already assigned variables to obtain a tighter network $\gamma'$.
\end{definition}

\begin{definition}[Arc consistency]
	For a constraint network $\gamma$ and a partial assignment $a$, a pair $(u, v) \in V^2$ of variables is arc consistent if for every value in the domain of $u$, there exists a valid partner in the domain for $v$. For a variable $w \in dom(a)$, assume $D_w = \{a(w)\}$.
\end{definition}

\begin{remark}
	Enforcing arc consistency:
	\begin{description}
		\item[AC-1] Iterate repeatedly over every constraint and enforce arc consistency in both directions. Stop when no changes have been made in one iteration.
		\item[AC-3] For every constraint $C_{uv}$, put $(u,v)$ and $(v,u)$ in $M$. Do the following until $M=\emptyset$: Remove one element $(u,v)$ from $M$ and enforce arc consistency from $u$ to $v$. If $D_u$ changed, add $(w,u)$ to $M$ for every constraint $C_{uw}$ and $w \neq v$.
	\end{description}
\end{remark}

\begin{remark}
	To solve an acyclic constraint network, enforce arc consistency with AC-3 and run backtracking with inference on the arc consistent network. This will find a solution without having to backtrack.
\end{remark}

\begin{definition}[Cutset conditioning]
	TODO
\end{definition}

\section{Logic}

\begin{definition}[Syntax]
	Rules to decide what are legal formulas.
\end{definition}

\begin{definition}[Semantics]
	Rules to decide whether a formula $A$ is true for a given assignment or interpretation $\phi$. Write $\phi \models A$ is $A$ is true under $\phi$ or $\phi \not\models A$ if not.
\end{definition}

\begin{definition}[Entailment]
	$B$ is entailed by $A$ iff for every interpretation that makes $A$ true, $B$ is true as well (For every model $\phi$, $\phi \models A \implies \phi \models B$). Write $A \models B$.
\end{definition}

\begin{definition}[Deduction]
	Which statements can be derived from $A$ using a set of inference rules $\mathcal{C}$? $A \vdash_\mathcal{C} B$ means $B$ can be derived from $A$ in the calculus $\mathcal{C}$.
\end{definition}

\begin{definition}[Soundness]
	A calculus $\mathcal{C}$ is sound if for all formulas $A, B$ it is true that $A \vdash_\mathcal{C} B \implies A \models B$.
\end{definition}

\begin{definition}[Complete]
	A calculus $\mathcal{C}$ is complete if for all formulas $A, B$ it is true that $A \models B \implies A \vdash_\mathcal{C} B$.
\end{definition}

\begin{definition}[Propositional logic]
	Also called $PL^0$. Let $\text{wff}_o(\mathcal{V}_o)$ be the set of well-formed formulas with variables $\mathcal{V}_o$.
\end{definition}

\begin{definition}[First order logic]
	Also called $FOL$. $\text{wff}_\iota(\Sigma_\iota)$ is the set of well-formed terms over a signature $\Sigma_\iota$ (function and skolem constants). $\text{wff}_o(\Sigma)$ is the set of well-formed propositions over a signature $\Sigma$ ($\Sigma_\iota$ plus connectives and predicate constants).
\end{definition}

\begin{theorem}[Unsatisfiability]
	Let $\mathcal{H}$ be a set of formulas and $A$ be a single formula. $\mathcal{H} \models A$ iff $\mathcal{H} \cup \{\neg A\}$ is unsatisfiable.
\end{theorem}

\begin{definition}[Conjunctive normal form]
	A formula $A$ is in conjunctive normal form (CNF) if it is a conjunction of disjunctions of literals: $A = \wedge_{i=1}^n \vee_{j=1}^{m_i} l_{ij}$ where $l_{ij}$ is a literal, which is a possibly negated variable.
\end{definition}

\begin{definition}[Natural deduction]
	Also $\mathcal{ND}^1$. Contains the following inference rules:

	\begin{multicols*}{2}
		\begin{prooftree}
			\AxiomC{A}
			\AxiomC{B}
			\RightLabel{$\wedge I$}
			\BinaryInfC{$A \wedge B$}
		\end{prooftree}

		\begin{prooftree}
			\AxiomC{$A \wedge B$}
			\RightLabel{$\wedge E_l$}
			\UnaryInfC{$A$}
		\end{prooftree}

		\begin{prooftree}
			\AxiomC{$A \wedge B$}
			\RightLabel{$\wedge E_r$}
			\UnaryInfC{$B$}
		\end{prooftree}

		\begin{prooftree}
			\AxiomC{}
			\RightLabel{TND}
			\UnaryInfC{$A \vee \neg A$}
		\end{prooftree}

		\begin{prooftree}
			\AxiomC{A}
			\UnaryInfC{B}
			\RightLabel{$\implies I$}
			\UnaryInfC{$A \implies B$}
		\end{prooftree}

		\begin{prooftree}
			\AxiomC{$A \implies B$}
			\AxiomC{A}
			\RightLabel{$\implies E$}
			\BinaryInfC{B}
		\end{prooftree}

		\begin{prooftree}
			\AxiomC{A}
			\RightLabel{$\forall I$}
			\UnaryInfC{$\forall X. A$}
		\end{prooftree}

		\begin{prooftree}
			\AxiomC{$\forall X. A$}
			\RightLabel{$\forall E$}
			\UnaryInfC{$[B/X](A)$}
		\end{prooftree}

		\begin{prooftree}
			\AxiomC{$[B/X](A)$}
			\RightLabel{$\exists I$}
			\UnaryInfC{$\exists X. A$}
		\end{prooftree}

		\begin{prooftree}
			\AxiomC{$\exists X. A$}
			\AxiomC{$[c/X](A)$}
			\UnaryInfC{B}
			\RightLabel{$\exists E$}
			\BinaryInfC{$B$}
		\end{prooftree}

		\begin{prooftree}
			\AxiomC{}
			\RightLabel{$=I$}
			\UnaryInfC{$A=A$}
		\end{prooftree}

		\begin{prooftree}
			\AxiomC{$A=B$}
			\AxiomC{$C[A]_p$}
			\RightLabel{$=E$}
			\BinaryInfC{$[B/p](C)$}
		\end{prooftree}
	\end{multicols*}
\end{definition}

\begin{definition}[Analytical tableaux]
	Contains the following inference rules:
	\begin{multicols*}{2}
		\begin{prooftree}
			\AxiomC{$A \wedge B^T$}
			\RightLabel{$\mathcal{T}_0 \wedge$}
			\UnaryInfC{$A^T, B^T$}
		\end{prooftree}

		\begin{prooftree}
			\AxiomC{$A \wedge B^F$}
			\RightLabel{$\mathcal{T}_0 \vee$}
			\UnaryInfC{$A^F | B^F$}
		\end{prooftree}

		\begin{prooftree}
			\AxiomC{$\neg A^T$}
			\RightLabel{$\mathcal{T}_0 \overset{T}{\neg}$}
			\UnaryInfC{$A^F$}
		\end{prooftree}

		\begin{prooftree}
			\AxiomC{$\neg A^F$}
			\RightLabel{$\mathcal{T}_0 \overset{F}{\neg}$}
			\UnaryInfC{$A^T$}
		\end{prooftree}

		\begin{prooftree}
			\AxiomC{$\neg A^T$}
			\AxiomC{$\neg A^F$}
			\RightLabel{$\mathcal{T}_0 cut$}
			\BinaryInfC{$\bot$}
		\end{prooftree}

		\begin{prooftree}
			\AxiomC{$\forall X. A^T$}
			\AxiomC{$C \in \text{cwff}_\iota(\Sigma_\iota)$}
			\RightLabel{$\mathcal{T}_1 \forall$}
			\BinaryInfC{$[C/X](A)^T$}
		\end{prooftree}

		\begin{prooftree}
			\AxiomC{$\forall X. A^F$}
			\AxiomC{$c \in (\Sigma_0^{sk} \setminus \mathcal{H})$}
			\RightLabel{$\mathcal{T}_1 \exists$}
			\BinaryInfC{$[c/X](A)^F$}
		\end{prooftree}

		\begin{prooftree}
			\AxiomC{$A \implies B^T$}
			\UnaryInfC{$A^F | B^T$}
		\end{prooftree}

		\begin{prooftree}
			\AxiomC{$A \implies B^F$}
			\UnaryInfC{$A^T, B^F$}
		\end{prooftree}

		\begin{prooftree}
			\AxiomC{$A^T$}
			\AxiomC{$A \implies B^T$}
			\BinaryInfC{$B^T$}
		\end{prooftree}

		\begin{prooftree}
			\AxiomC{$A \vee B^T$}
			\UnaryInfC{$A^T | B^T$}
		\end{prooftree}

		\begin{prooftree}
			\AxiomC{$A \vee B^F$}
			\UnaryInfC{$A^F, B^F$}
		\end{prooftree}

		\begin{prooftree}
			\AxiomC{$A \Leftrightarrow B^T$}
			\UnaryInfC{$A^T, B^T | A^F, B^F$}
		\end{prooftree}

		\begin{prooftree}
			\AxiomC{$A \Leftrightarrow B^F$}
			\UnaryInfC{$A^T, B^F | A^F, B^T$}
		\end{prooftree}
	\end{multicols*}

	All rules do the same thing: If the premise is $P$, open one branch for every way to make $P$ true. For example: There are two ways to make the premise $A \implies B^T$ true. Either $A^F$ or $B^T$. This means two branches are opened, one for $A^F$ and one for $B^T$. (N.b. there are actually three ways to make the premise true: $A^T,B^T | A^F,B^T | A^F,B^F$. It is still enough to open just two branches, because $B^T$ captures the former two ways and $A^F$ captures the latter two.)

	Of the first five rules, all operate in the same branch, except $\mathcal{T}_0 \vee$. This rule creates two new branches, one for $A^F$ and one for $B^F$.

	A tableaux is saturated if all rules that can be applied do not contribute new material.

	A branch is closed if it contains $\bot$, else open. A tableau is closed if all of it's branches are closed (n.b. a closed tableau may or may not be saturated).
\end{definition}

\begin{theorem}
	$A$ is valid iff there is a closed tableau with $A^F$ at the root.
\end{theorem}

\begin{definition}[Resolution]
	The resolution calculus has three rules of inference:

	\begin{prooftree}
		\AxiomC{$P^T \vee A$}
		\AxiomC{$P^F \vee B$}
		\BinaryInfC{$A \vee B$}
	\end{prooftree}

	\begin{prooftree}
		\AxiomC{$P^T \vee A$}
		\AxiomC{$Q^F \vee B$}
		\AxiomC{$\sigma = mgu(P, Q)$}
		\TrinaryInfC{$\sigma(A) \vee \sigma(B)$}
	\end{prooftree}

	\begin{prooftree}
		\AxiomC{$P^\alpha \vee Q^\alpha \vee A$}
		\AxiomC{$\sigma = mgu(P, Q)$}
		\BinaryInfC{$\sigma(P) \vee \sigma(A)$}
	\end{prooftree}

	The last two rules are only necessary when working in FOL. The second rule assumes $A, B$ share no variables. In the last rule, $\alpha$ is either $\top$ or $\bot$.
\end{definition}

\begin{remark}[Resolution]
	A derivation of the empty clause $\square$ from a clause set $S$ is a resolution refutation. This means $S$ is unsatisfiable.

	A resolution refutation of $CNF(\mathcal{H} \wedge \neg A)$ is a resolution proof for $\mathcal{H} \models A$. Refer to the unsatisfiability theorem.
\end{remark}

\begin{definition}[Conversion into CNF]
	An arbitrary formula can be transformed into a CNF by doing the following steps:

	\begin{enumerate}
		\item Rewrite all implications and equivalences using negations, disjunctions and conjunction.
		\item Move negations inwards. After this step, negations may only occur immediately before predicates.
		\item Rename variables bound by quantifiers to make them unique. After this step, a variable is either free or bound by exactly one quantifier.
		\item Move quantifiers outwards. After this step, a quantifier may only occur in the prefix of the formula but not inside of a $\wedge, \vee$ or $\neg$.
		\item Replace variables bound by existential quantifiers with skolem functions. Example: $\forall x_1 \dots \forall x_n \exists x_{n+1}. P$ is replaced by $\forall x_1 \dots \forall x_n. [f(x_1, \dots, x_n)/x_{n+1}](P)$.
		\item Drop universal quantifiers.
		\item Distribute $\vee$'s inwards over $\wedge$'s: $A \vee (B \wedge C)$ becomes $(A \vee B) \wedge (A \vee C)$.
	\end{enumerate}
\end{definition}

\begin{remark}
	$CNF(P)$ is satisfiable iff $P$ is satisfiable.
\end{remark}

\begin{definition}[DPLL]
	The DPLL procedure is an algorithm to find an interpretation satisfying a clause set $\Delta$.
\end{definition}

\begin{definition}[Abstract consistency]
	A family $\nabla$ of sets of propositions is an abstract consistency class, iff for every $\phi \in \nabla$ it is true that
	\begin{itemize}
		\item $P \not\in \phi$ or $\neg P \not\in \phi$ for every variable $P$
		\item $\phi \ast A \in \nabla$ if $\neg\neg A \in \phi$
		\item $\phi \ast A \in \nabla$ or $\phi \ast B \in \nabla$ if $(A \vee B) \in \phi$
		\item $\phi \ast \neg A \ast \neg B \in \nabla$ if $\neg(A \vee B) \in \phi$
		\item $\phi \ast [B/X](A) \in \nabla$ for every closed term $B$ if $(\forall X. A) \in \phi$
		\item $\phi \ast [c/X](A) \in \nabla$ for a fresh constant $c$ if $(\neg \forall X. A) \in \phi$
	\end{itemize}
\end{definition}

\begin{theorem}[Model existence]
	If $\nabla$ is an abstract consistency class and $\phi \in \nabla$ then $\phi$ is satisfiable.
\end{theorem}

\begin{theorem}
	$\nabla = \{ \phi \; | \; \phi \text{ has no closed tableau} \}$ is an abstract consistency class.
\end{theorem}

\begin{theorem}
	The calculus of analytical tableaux is complete.
\end{theorem}

\begin{proof}
	Show that whenever $A$ is valid, $\neg A$ must have a closed tableau: Assume $A$ is valid. Assume $\neg A$ has no closed tableau. $\neg A \in \nabla$. As per model existence, $\neg A$ is satisfiable because it is in $\nabla$. This contradicts the assumption that $A$ is valid. $\neg A$ must have a closed tableau.
\end{proof}

\section{Logic Programming}

\begin{definition}[Fact]
	This is a term that is unconditionally true.
\end{definition}

\begin{definition}[Rule]
	This is a term that is true if certain premises are true.
\end{definition}

\begin{definition}[Clause]
	Facts and rules are both clauses.
\end{definition}

\begin{definition}[Knowledge base]
	The knowledge base given by a Prolog program is the set of terms that can be derived from it using the following rules:

	\begin{multicols*}{2}
		\begin{prooftree}
			\AxiomC{$A$}
			\AxiomC{$A \implies B$}
			\RightLabel{MP}
			\BinaryInfC{$B$}
		\end{prooftree}

		\begin{prooftree}
			\AxiomC{$A$}
			\AxiomC{$B$}
			\RightLabel{$\wedge I$}
			\BinaryInfC{$A \wedge B$}
		\end{prooftree}
	\end{multicols*}

	\begin{prooftree}
		\AxiomC{$A$}
		\RightLabel{Subst}
		\UnaryInfC{$[B/X](A)$}
	\end{prooftree}
\end{definition}

\begin{definition}[Horn clause]
	A horn clause is a clause with at most one positive literal.
\end{definition}

\begin{remark}
	The Prolog rule $H :- B_1, \dots, B_n$ is the implication $B_1 \wedge \dots \wedge B_n \implies H$ can be written as $\neg B_1 \vee \dots \vee \neg B_n \vee H$. This is a horn clause.
\end{remark}

\section{Planning}

\begin{definition}[Planning language]
	A planning language describes, using logic, the
	\begin{itemize}
		\item set of possible states
		\item initial state $I$
		\item goal condition $G$
		\item set of actions $A$ in terms of preconditions and effects.
	\end{itemize}
\end{definition}

\begin{remark}
	By describing the components of a planning problem using logic, the solver is able to gain insight into the problem structure. This means the solver is no longer working on a black-box.
\end{remark}

\begin{definition}[Satisficing planning]
	A procedure that takes as input a planning problem $\Pi$ and outputs a plan for $\Pi$ or unsolvable, if no such plan exists.
\end{definition}

\begin{definition}[Optimal planning]
	A procedure that takes as input a planning problem $\Pi$ and outputs an optimal plan for $\Pi$ or unsolvable, if no such plan exists.
\end{definition}

\begin{definition}[STRIPS planning task]
	This is a encoding of a planning problem using a 4-tuple $\Pi = \langle P, A, I, G \rangle$ where
	\begin{itemize}
		\item $P$ is a finite set of facts
		\item $A$ is a finite set of actions, each given as a triple $\langle pre_a, add_a, del_a \rangle$. The components of the triple are called preconditions, add-list and delete-list
		\item $I \subseteq P$ is the initial state
		\item $G \subseteq P$ is the goal.
	\end{itemize}
\end{definition}

\begin{definition}[Only-adds relaxation]
	This is a relaxation of a given STRIPS planning task $\Pi$ where $P, I, G$ are the same and the actions are the actions of $\Pi$ with empty preconditions and empty delete lists.
\end{definition}

\begin{definition}[Delete relaxation]
	This is a relaxation $\Pi^+$ of a given STRIPS planning task $\Pi$ where $P, I, G$ are the same and the actions are the actions of $\Pi$ with empty delete lists.
\end{definition}

\begin{definition}[Relaxed plan]
	Let $\Pi = \langle P, A, I, G \rangle$ be a planning task. A relaxed plan for $s \in \mathcal{P}(P)$ is a plan for $\langle P, A, s, G \rangle^+$. A relaxed plan for $I$ is called a relaxed plan for $\Pi$.
\end{definition}

\begin{remark}[Planning algorithms]
	Plans for planning tasks can be found using informed search strategies.
\end{remark}

\begin{definition}[$h^+$-heuristic]
	For a planning task $\Pi = \langle P, A, I, G \rangle$, $h^+: \mathcal{P} \mapsto \mathbb{N} \cup \{\infty\}$ is a heuristic calculating the length of the optimal relaxed plan for $s$ or $\infty$ if no plan exists.
\end{definition}

\begin{theorem}
	$h^+$ is admissible.
\end{theorem}

\begin{theorem}
	Calculating $h^+$ is NP-complete.
\end{theorem}

\begin{definition}[$h^{FF}$-heuristic]
	For a planning task $\Pi = \langle P, A, I, G \rangle$, $h^{FF}: \mathcal{P} \mapsto \mathbb{N} \cup \{\infty\}$ is a heuristic calculating the length of a relaxed plan for $s$ or $\infty$ if no plan exists.
\end{definition}

\begin{remark}
	$h^{FF}$ never underestimates $h^+$ and may even overestimate $h^*$. Thus, $h^{FF}$ is not admissible and may not be used for optimal planning (but for satisficing planning).
\end{remark}

\end{multicols*}


\end{document}