From d2fd485a47ad565977463c0a211d6463fb77dcdf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Dennis=20M=C3=BCller?= <d.mueller@jacobs-university.de>
Date: Mon, 23 Apr 2018 16:17:51 +0200
Subject: [PATCH] update
---
tex/paper.tex | 4 +---
tex/viewfinder.tex | 2 +-
2 files changed, 2 insertions(+), 4 deletions(-)
diff --git a/tex/paper.tex b/tex/paper.tex
index cb0f764..9968e02 100644
--- a/tex/paper.tex
+++ b/tex/paper.tex
@@ -14,9 +14,7 @@
%\usepackage{appendix}
\usepackage[style=alphabetic,hyperref=auto,defernumbers=true,backend=bibtex,firstinits=true,maxbibnames=9,maxcitenames=3,isbn=false]{biblatex}
-% \addbibresource{../../fr-macros/rabe.bib}
-% \addbibresource{../../fr-macros/systems.bib}
-% \addbibresource{../../fr-macros/pub_rabe.bib}
+
\addbibresource{kwarcpubs.bib}
\addbibresource{extpubs.bib}
\addbibresource{kwarccrossrefs.bib}
diff --git a/tex/viewfinder.tex b/tex/viewfinder.tex
index d71c357..dd64787 100644
--- a/tex/viewfinder.tex
+++ b/tex/viewfinder.tex
@@ -4,7 +4,7 @@ To run a proper unficiation algorithm is in our situation infeasible, since the
\paragraph{} We do so by first transforming each constant $C$ in a theory to an \emph{encoding} $(\cn{h}(C),\cn{syms}(C))$ the following way:
-Consider the syntax tree of the type $t$ of a constant $C$. We first systematically replace the leaves by an abstract representation, yielding a data structure $\cn{tree}(C)$. We can eliminate variables by replacing them by their De Bruijn index, and symbol references by considering them like a separate set of variables, replacing them by their De Brujin indices and storing the symbol's names in a list $\cn{syms}(C)$.
+Consider the syntax tree of the type $t$ of a constant $C$. We first systematically replace the leaves by an abstract representation, yielding a data structure $\cn{tree}(C)$. We can eliminate variables by replacing them by their De Bruijn index, and symbol references by enumerating them and storing the symbol's names in a list $\cn{syms}(C)$.
As a result, we get a pair $(\cn{tree}(C),\cn{syms}(C))$. Now an assignment $V(C)=D$ is valid, iff $\cn{tree}(C)=\cn{tree}(D)$, the lists $\cn{syms}(C)$ and $\cn{syms}(D)$ have the same length and their pairwise assignments $V(\cn{syms}(C)_i)=\cn{syms}(D)_i$ are all valid.
--
GitLab