Book a Demo!
CoCalc Logo Icon
StoreFeaturesDocsShareSupportNewsAboutPoliciesSign UpSign In
Download

📚 The CoCalc Library - books, templates and other resources

132932 views
License: OTHER
Tweet
Share
Share
1
\documentclass{article}

2
\usepackage[pdftex,active,tightpage]{preview}

3
\setlength\PreviewBorder{2mm}

4


5
\usepackage[utf8]{inputenc} % this is needed for umlauts

6
\usepackage[ngerman]{babel} % this is needed for umlauts

7
\usepackage[T1]{fontenc}    % this is needed for correct output of umlauts in pdf

8
\usepackage{amssymb,amsmath,amsfonts} % nice math rendering

9
\usepackage{braket} % needed for \Set

10
\usepackage{algorithm,algpseudocode}

11


12
\algnewcommand\True{\textbf{true}\space}

13
\algnewcommand\False{\textbf{false}\space}

14
\algnewcommand{\LineComment}[1]{\State \(\triangleright\) #1}

15
\begin{document}

16
\begin{preview}

17
    \begin{algorithm}[H]

18
        \begin{algorithmic}

19
        \Require Klauselmenge $K$ in KNF (jede Klausel wird durch ein mit den

20
        Werten $\Set{-1,0,1}$ Array

21
        repräsentiert, dessen Länge gleich der Anzahl $n$ der Symbole ist),\\

22
            zu beweisende Aussage ist $\alpha$,\\

23
            $\beta := \neg \alpha$ in KNF

24
		\Procedure{Resolutionsalgorithmus}{$K$, $\beta$}

25
			\State $\gamma \gets K \cup \Set{\beta}$

26
			\State $foundMatch \gets$ \True

27
			\While{$foundMatch$}

28
		        \State $foundMatch \gets$ \False

29


30
				\LineComment{Finde zwei Klauseln, bei denen ein Symbol verneint bzw. nicht-verneint vorkommt. Wende darauf die Resolutionsregel an}

31
		        \For{$i \in \Set{1, \dots, |\gamma|-1}$}

32
		            \For{$j \in \Set{i+1, \dots |\gamma|}$}

33
		                \For{$k \in \Set{0, \dots, n-1}$}

34
		                    \If{$\gamma_i[k] \cdot \gamma_j[k] == (-1)$}

35
		                        \State $foundMatch \gets$ \True

36
		                        \State $tmp \gets $ Array der Länge $n$

37
		                        \For{$l \in \Set{0, \dots, n-1}$}

38
		                            \If{$\gamma_i[l] \cdot \gamma_j[l] == (-1)$ and

39
		                                $l \neq k$}

40
		                                \State $tmp \gets $ leere Klausel

41
		                                \State break

42
		                            \ElsIf{$\gamma_i[l] \neq 0$}

43
		                                \State $tmp[l] \gets \gamma_i[l]$

44
		                            \Else

45
		                                \State $tmp[l] \gets \gamma_j[l]$

46
		                            \EndIf

47
		                        \EndFor

48
		                        \State $\gamma \gets (\gamma \cup \Set{tmp}) \setminus

49
		                                \Set{\gamma_i, \gamma_j}$

50
		                        \State break

51
		                    \EndIf

52
		                \EndFor

53


54
		                \If{$foundMatch$}

55
		                    \State break

56
		                \EndIf

57
		            \EndFor

58


59
	                \If{$foundMatch$}

60
	                    \State break

61
	                \EndIf

62
		        \EndFor

63
			\EndWhile

64
		\EndProcedure

65
        \end{algorithmic}

66
    \caption{Resolutionsalgorithmus}

67
    \label{alg:resolutionsalgorithmus}

68
    \end{algorithm}

69
\end{preview}

70
\end{document}

71


72