From db15dca96806093f73028ed9b55f590b45a59e7d Mon Sep 17 00:00:00 2001 From: Florian Knoch Date: Fri, 10 May 2019 19:13:43 +0200 Subject: [PATCH] Add section on prooftrees --- sections/german/15/15.md | 56 ++++ sections/german/15/prftree-crop.svg | 462 ++++++++++++++++++++++++++++ sections/german/15/prftree-orig.svg | 462 ++++++++++++++++++++++++++++ sections/german/15/prftree.tex | 52 ++++ 4 files changed, 1032 insertions(+) create mode 100644 sections/german/15/prftree-crop.svg create mode 100644 sections/german/15/prftree-orig.svg create mode 100644 sections/german/15/prftree.tex diff --git a/sections/german/15/15.md b/sections/german/15/15.md index 981ded1..e347e58 100644 --- a/sections/german/15/15.md +++ b/sections/german/15/15.md @@ -113,6 +113,62 @@ child { node {home} --- +
+
+

Mathematische Beweisführung

+

Beweisbäume lassen sich mit dem Paket `prftree` einwandfrei darstellen.

+ 
\begin{displaymath}
+\prftree[l,r]{}{[comp$\_{ns}$]}
+{
+  \prftree[l,r]{}{[comp$\_{ns}$]}
+  {
+    \prftree[l,r]{}{[ass$\_{ns}$]}
+    {
+      -
+    }
+    {
+      (\texttt{m:=a}, \sigma\_{\bot,\bot})
+      \rightarrow \sigma\_{48,\bot}
+    }
+  }
+  {
+    \prftree[l,r]{}{[ass$\_{ns}$]}
+    {
+      -
+    }
+    {
+      (\texttt{n:=b}, \sigma\_{48,\bot})
+      \rightarrow \sigma\_{48,18}
+    }
+  }
+  {
+    (\texttt{m:=a; n:=b}, \sigma\_{\bot,\bot})
+    \rightarrow \sigma\_{48,18}
+  }
+}
+{
+  \prftree[l,r]{}{}
+  {
+    \dots
+  }
+  {
+    \textbf{[1]}\ (\texttt{LOOP}, \sigma\_{48,18})
+    \rightarrow \sigma\_{6,6}
+  }
+}
+{
+  (\texttt{m:=a; n:=b; LOOP}, \sigma\_{\bot,\bot})
+  \rightarrow \sigma\_{6,6}
+}
+\end{displaymath}
+
+
+ +
+
+ +--- +

Weitere nützliche Pakete

diff --git a/sections/german/15/prftree-crop.svg b/sections/german/15/prftree-crop.svg new file mode 100644 index 0000000..cda125f --- /dev/null +++ b/sections/german/15/prftree-crop.svg @@ -0,0 +1,462 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/sections/german/15/prftree-orig.svg b/sections/german/15/prftree-orig.svg new file mode 100644 index 0000000..29ae1ef --- /dev/null +++ b/sections/german/15/prftree-orig.svg @@ -0,0 +1,462 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/sections/german/15/prftree.tex b/sections/german/15/prftree.tex new file mode 100644 index 0000000..023208a --- /dev/null +++ b/sections/german/15/prftree.tex @@ -0,0 +1,52 @@ +\documentclass[a4paper, pdftex, 12pt]{scrartcl} +\usepackage{scrtime} +\usepackage[utf8]{inputenc} +\usepackage[T1]{fontenc} +\usepackage{amsmath, amsfonts, amssymb} +\usepackage{prftree} +\usepackage{stmaryrd} +\usepackage{mathtools} +\begin{document} +\thispagestyle{empty} + +\begin{displaymath} +\prftree[l,r]{}{[comp$_{ns}$]} +{ + \prftree[l,r]{}{[comp$_{ns}$]} + { + \prftree[l,r]{}{[ass$_{ns}$]} + { + - + } + { + (\texttt{m:=a}, \sigma_{\bot,\bot}) \rightarrow \sigma_{48,\bot} + } + } + { + \prftree[l,r]{}{[ass$_{ns}$]} + { + - + } + { + (\texttt{n:=b}, \sigma_{48,\bot}) \rightarrow \sigma_{48,18} + } + } + { + (\texttt{m:=a; n:=b}, \sigma_{\bot,\bot}) \rightarrow \sigma_{48,18} + } +} +{ + \prftree[l,r]{}{} + { + \dots + } + { + \textbf{[1]}\ (\texttt{LOOP}, \sigma_{48,18}) \rightarrow \sigma_{6,6} + } +} +{ + (\texttt{m:=a; n:=b; LOOP}, \sigma_{\bot,\bot}) \rightarrow \sigma_{6,6} +} +\end{displaymath} + +\end{document} \ No newline at end of file