diff --git a/source-code/Pseudocode/Resolutionsalgorithmus/Makefile b/source-code/Pseudocode/Resolutionsalgorithmus/Makefile new file mode 100644 index 0000000..d4bb3d1 --- /dev/null +++ b/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 diff --git a/source-code/Pseudocode/Resolutionsalgorithmus/Readme.md b/source-code/Pseudocode/Resolutionsalgorithmus/Readme.md new file mode 100644 index 0000000..f8ac563 --- /dev/null +++ b/source-code/Pseudocode/Resolutionsalgorithmus/Readme.md @@ -0,0 +1,3 @@ +Compiled example +---------------- +![Example](Resolutionsalgorithmus.png) diff --git a/source-code/Pseudocode/Resolutionsalgorithmus/Resolutionsalgorithmus.png b/source-code/Pseudocode/Resolutionsalgorithmus/Resolutionsalgorithmus.png new file mode 100644 index 0000000..5744070 Binary files /dev/null and b/source-code/Pseudocode/Resolutionsalgorithmus/Resolutionsalgorithmus.png differ diff --git a/source-code/Pseudocode/Resolutionsalgorithmus/Resolutionsalgorithmus.tex b/source-code/Pseudocode/Resolutionsalgorithmus/Resolutionsalgorithmus.tex new file mode 100644 index 0000000..4f88789 --- /dev/null +++ b/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}