Resolutionsalgorithmus

source-code/Pseudocode/Resolutionsalgorithmus/Makefile

@@ -0,0 +1,36 @@
+SOURCE = Resolutionsalgorithmus
+DELAY = 80
+DENSITY = 300
+WIDTH = 500
+
+make:
+	pdflatex $(SOURCE).tex -output-format=pdf
+	pdflatex $(SOURCE).tex -output-format=pdf
+	make clean
+
+clean:
+	rm -rf  $(TARGET) *.class *.html *.log *.aux *.data *.gnuplot
+
+gif:
+	pdfcrop $(SOURCE).pdf
+	convert -verbose -delay $(DELAY) -loop 0 -density $(DENSITY) $(SOURCE)-crop.pdf $(SOURCE).gif
+	make clean
+
+png:
+	make
+	make svg
+	inkscape $(SOURCE).svg -w $(WIDTH) --export-png=$(SOURCE).png
+
+transparentGif:
+	convert $(SOURCE).pdf -transparent white result.gif
+	make clean
+
+svg:
+	make
+	#inkscape $(SOURCE).pdf --export-plain-svg=$(SOURCE).svg
+	pdf2svg $(SOURCE).pdf $(SOURCE).svg
+	# Necessary, as pdf2svg does not always create valid svgs:
+	inkscape $(SOURCE).svg --export-plain-svg=$(SOURCE).svg
+	rsvg-convert -a -w $(WIDTH) -f svg $(SOURCE).svg -o $(SOURCE)2.svg
+	inkscape $(SOURCE)2.svg --export-plain-svg=$(SOURCE).svg
+	rm $(SOURCE)2.svg

source-code/Pseudocode/Resolutionsalgorithmus/Readme.md

@@ -0,0 +1,3 @@
+Compiled example
+----------------
+![Example](Resolutionsalgorithmus.png)

source-code/Pseudocode/Resolutionsalgorithmus/Resolutionsalgorithmus.tex

@@ -0,0 +1,70 @@
+\documentclass{article}
+\usepackage[pdftex,active,tightpage]{preview}
+\setlength\PreviewBorder{2mm}
+
+\usepackage[utf8]{inputenc} % this is needed for umlauts
+\usepackage[ngerman]{babel} % this is needed for umlauts
+\usepackage[T1]{fontenc}    % this is needed for correct output of umlauts in pdf
+\usepackage{amssymb,amsmath,amsfonts} % nice math rendering
+\usepackage{braket} % needed for \Set
+\usepackage{algorithm,algpseudocode}
+
+\algnewcommand\True{\textbf{true}\space} 
+\algnewcommand\False{\textbf{false}\space} 
+\algnewcommand{\LineComment}[1]{\State \(\triangleright\) #1}
+\begin{document}
+\begin{preview}
+    \begin{algorithm}[H]
+        \begin{algorithmic}
+        \Require Klauselmenge $K$ in KNF (jede Klausel wird durch ein mit den
+        Werten $\Set{-1,0,1}$ Array
+        repräsentiert, dessen Länge gleich der Anzahl $n$ der Symbole ist),\\
+            zu beweisende Aussage ist $\alpha$,\\
+            $\beta := \neg \alpha$ in KNF
+		\Procedure{Resolutionsalgorithmus}{$K$, $\beta$}
+			\State $\gamma \gets K \cup \Set{\beta}$
+			\State $foundMatch \gets$ \True
+			\While{$foundMatch$}
+		        \State $foundMatch \gets$ \False
+
+				\LineComment{Finde zwei Klauseln, bei denen ein Symbol verneint bzw. nicht-verneint vorkommt. Wende darauf die Resolutionsregel an}
+		        \For{$i \in \Set{1, \dots, |\gamma|-1}$}
+		            \For{$j \in \Set{i+1, \dots |\gamma|}$}
+		                \For{$k \in \Set{0, \dots, n-1}$}
+		                    \If{$\gamma_i[k] \cdot \gamma_j[k] == (-1)$}
+		                        \State $foundMatch \gets$ \True
+		                        \State $tmp \gets $ Array der Länge $n$
+		                        \For{$l \in \Set{0, \dots, n-1}$}
+		                            \If{$\gamma_i[l] \cdot \gamma_j[l] == (-1)$ and
+		                                $l \neq k$}
+		                                \State $tmp \gets $ leere Klausel
+		                                \State break
+		                            \ElsIf{$\gamma_i[l] \neq 0$}
+		                                \State $tmp[l] \gets \gamma_i[l]$
+		                            \Else
+		                                \State $tmp[l] \gets \gamma_j[l]$
+		                            \EndIf
+		                        \EndFor
+		                        \State $\gamma \gets (\gamma \cup \Set{tmp}) \setminus
+		                                \Set{\gamma_i, \gamma_j}$
+		                        \State break
+		                    \EndIf
+		                \EndFor
+
+		                \If{$foundMatch$}
+		                    \State break
+		                \EndIf
+		            \EndFor
+
+	                \If{$foundMatch$}
+	                    \State break
+	                \EndIf
+		        \EndFor
+			\EndWhile
+		\EndProcedure
+        \end{algorithmic}
+    \caption{Resolutionsalgorithmus}
+    \label{alg:resolutionsalgorithmus}
+    \end{algorithm}
+\end{preview}
+\end{document}