

Rule: coreset\_FEs\_are\_core\_and\_member\label{rule_generated:coreset_FEs_are_core_and_member} importance: 200\newline For each FrameElement that is part of a CoreSet we require that this FrameElement is actually core (or core unexpressed) and a member of the Frame associated with the CoreSet relation.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em coreset}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getCoreSets}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mbox{\em coreset}
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mbox{\em fe}
\right)
= 
\hspace*{2pt}
\mathtt{Core}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em fe}
. 
\mathtt{feType}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{Core}
\hspace*{3pt}
2
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\vee 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mbox{\em fe}
\right)
= 
\\
\mathtt{CoreUnexpressed}
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em fe}
. 
\mathtt{feType}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{CoreUnexpressed}
\hspace*{3pt}
2
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\right)
\\
\wedge 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}
\in 
\hspace*{2pt}
\mathtt{getFEs}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}
\right)
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em fe}
. 
\mathtt{frameRef}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{ident}
\left(
\mbox{\em frame}
\right)
\hspace*{3pt}
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: frames\_have\_LUs\_if\_not\_non-lexical\label{rule_generated:frames_have_LUs_if_not_non-lexical} importance: 200\newline For each Frame we require at least one LU, except for those Frames that have a semantic type "Non-Lexical"{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em st}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameSTs}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}
\right)
\hspace*{5pt}
\bullet 
\\
\neg 
\hspace*{2pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{name}
\left(
\mbox{\em st}
\right)
= 
\\
\mathsf{Non-Lexical Frame}
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em st}
. 
\mathtt{name}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathsf{Non-Lexical Frame}
\hspace*{3pt}
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\right)
\\
\implies 
\\
\neg 
\hspace*{2pt}
\mathtt{null}
\left(
\mathtt{getLUs}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}
\right)
\right)
\\
\end{array}
\\
\end{array}
\]


}

Rule: frames\_have\_core\_FE\label{rule_generated:frames_have_core_FE} importance: 200\newline Each Frame has at least one core (or core-unexpressed) frame element.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEs}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mbox{\em fe}
\right)
= 
\hspace*{2pt}
\mathtt{Core}
\\
\left\{
\left\{
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em fe}
. 
\mathtt{feType}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{Core}
\hspace*{3pt}
2
\right\}
\right\}
\\
\end{array}
\\
\vee 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mbox{\em fe}
\right)
= 
\hspace*{2pt}
\mathtt{CoreUnexpressed}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em fe}
. 
\mathtt{feType}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{CoreUnexpressed}
\hspace*{3pt}
2
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: frames\_without\_LUs\_are\_non-lexical\label{rule_generated:frames_without_LUs_are_non-lexical} importance: 200\newline If a frame has any LUs then its semantic type should not be "Non-Lexical"{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\neg 
\hspace*{2pt}
\mathtt{null}
\left(
\mathtt{getLUs}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}
\right)
\right)
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em st}
^{
\mathsf{Del}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameSTs}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}
\right)
\hspace*{5pt}
\bullet 
\\
\neg 
\hspace*{2pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{name}
\left(
\mbox{\em st}
\right)
= 
\\
\mathsf{Non-Lexical Frame}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\]


}

Rule: nonempty\_frames\label{rule_generated:nonempty_frames} importance: 200\newline Each Frame has at least one frame element.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEs}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}
\right)
\hspace*{5pt}
\bullet 
\\
\mathtt{True}
\\
\end{array}
\\
\end{array}
\]


}

Rule: no\_childRef\_for\_CoreSet\_Excludes\_Requires\label{rule_generated:no_childRef_for_CoreSet_Excludes_Requires} importance: 170\newline There should be no source reference for the Frame relations CoreSet, Excludes, and Requires (i.e., those relations are unary in the way that they say that there are FEs in this Frame that belong to the CoreSet, exclude each other, or require one another){\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameRelationsByType}
\left(
\mathtt{fnDB}
,
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{CoreSet}
,
\\
\mathsf{Excludes}
,
\\
\mathsf{Requires}
\\
\end{array}
\right]
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{source}
\left(
\mbox{\em rel}
\right)
= 
\hspace*{2pt}
\mathsf{0}
\\
\left\{
\left\{
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em rel}
. 
\mathtt{source}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathsf{0}
\hspace*{3pt}
\right\}
\right\}
\\
\end{array}
\\
\end{array}
\]


}

Rule: valid\_childRef\_for\_all\_but\_CoreSet\_Excludes\_Requires\label{rule_generated:valid_childRef_for_all_but_CoreSet_Excludes_Requires} importance: 170\newline Every Frame relation (except CoreSet, Excludes, Requires, ReFraming) should have a valid (i.e. non-null and existent) source reference.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterNotElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{getRelationTypeID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{CoreSet}
,
\\
\mathsf{Excludes}
,
\\
\mathsf{Requires}
,
\\
\mathsf{ReFraming}_{\mbox{\scriptsize\em Mapping}}
\\
\end{array}
\right]
\\
\end{array}
\right)
,
\\
\mathtt{relType}
,
\\
\mathtt{getAllFrameRelations}
\left(
\mathtt{fnDB}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{source}
\left(
\mbox{\em rel}
\right)
\not= 
\hspace*{2pt}
\mathsf{0}
\\
\wedge 
\\
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\neg 
\hspace*{2pt}
\mathtt{source}
\left(
\mbox{\em rel}
\right)
= 
\hspace*{2pt}
\mathsf{0}
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em frame}
^{
\mathsf{Add}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\mbox{\em frame}
\right)
= 
\\
\mathtt{source}
\left(
\mbox{\em rel}
\right)
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em frame}
. 
\mathtt{ident}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{source}
\left(
\mbox{\em rel}
\right)
\hspace*{3pt}
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\]


}

Rule: valid\_parentRef\_for\_all\_frame\_relations\label{rule_generated:valid_parentRef_for_all_frame_relations} importance: 170\newline Every Frame relation should have a valid (i.e. non-null and existent) target reference.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrameRelations}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{target}
\left(
\mbox{\em rel}
\right)
\not= 
\hspace*{2pt}
\mathsf{0}
\\
\wedge 
\\
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\neg 
\hspace*{2pt}
\mathtt{target}
\left(
\mbox{\em rel}
\right)
= 
\hspace*{2pt}
\mathsf{0}
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em frame}
^{
\mathsf{Add}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\mbox{\em frame}
\right)
= 
\\
\mathtt{target}
\left(
\mbox{\em rel}
\right)
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em frame}
. 
\mathtt{ident}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{target}
\left(
\mbox{\em rel}
\right)
\hspace*{3pt}
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\]


}

Rule: each\_frame\_is\_connected\label{rule_generated:each_frame_is_connected} importance: 160\newline Each Frame is connected to at least some other frame by a Frame-to-Frame relation, i.e., there are no lonely Frames.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}
^{
\mathsf{Del}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em rel}
^{
\mathsf{Add}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameRelationsByType}
\left(
\mathtt{fnDB}
,
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Inheritance}
,
\\
\mathsf{Using}
,
\\
\mathsf{Inchoative}_{\mbox{\scriptsize\em of}}
,
\\
\mathsf{Causative}_{\mbox{\scriptsize\em of}}
,
\\
\mathsf{Subframe}
,
\\
\mathsf{See}_{\mbox{\scriptsize\em also}}
,
\\
\mathsf{Perspective}_{\mbox{\scriptsize\em on}}
\\
\end{array}
\right]
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{source}
\left(
\mbox{\em rel}
\right)
= 
\hspace*{2pt}
\mathtt{ident}
\left(
\mbox{\em frame}
\right)
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em rel}
. 
\mathtt{source}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{ident}
\left(
\mbox{\em frame}
\right)
\hspace*{3pt}
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\vee 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{target}
\left(
\mbox{\em rel}
\right)
= 
\hspace*{2pt}
\mathtt{ident}
\left(
\mbox{\em frame}
\right)
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em rel}
. 
\mathtt{target}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{ident}
\left(
\mbox{\em frame}
\right)
\hspace*{3pt}
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: no\_cycles\_for\_Inheritance\_Using\_Inchoative\_of\_Causative\_of\label{rule_generated:no_cycles_for_Inheritance_Using_Inchoative_of_Causative_of} importance: 155\newline The Frame-to-Frame relations Inheritance, Using, Inchoative of, and Causative of should be acyclic.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em cycles}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{frCycles}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Inheritance}
,
\\
\mathsf{Using}
,
\\
\mathsf{Inchoative}_{\mbox{\scriptsize\em of}}
,
\\
\mathsf{Causative}_{\mbox{\scriptsize\em of}}
\\
\end{array}
\right]
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\mathtt{null}
\left(
\mbox{\em cycles}
\right)
\\
\end{array}
\]


}

Rule: only\_one\_relation\_inherits\_using\_subframe\_causative\_inchoative\_perspective\_on\label{rule_generated:only_one_relation_inherits_using_subframe_causative_inchoative_perspective_on} importance: 155\newline Between two Frames there should exist at most one relation of type Inheritance, Using, SubFrame, Inchoative of, and Causative of.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em AB}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Inheritance}
,
\\
\mathsf{Using}
,
\\
\mathsf{Inchoative}_{\mbox{\scriptsize\em of}}
,
\\
\mathsf{Causative}_{\mbox{\scriptsize\em of}}
,
\\
\mathsf{Subframe}
,
\\
\mathsf{Perspective}_{\mbox{\scriptsize\em on}}
\\
\end{array}
\right]
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\neg 
\hspace*{2pt}
\left(
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em rel2}_{\mbox{\scriptsize\em AB}}
^{
\mathsf{Del}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Inheritance}
,
\\
\mathsf{Using}
,
\\
\mathsf{Inchoative}_{\mbox{\scriptsize\em of}}
,
\\
\mathsf{Causative}_{\mbox{\scriptsize\em of}}
,
\\
\mathsf{Subframe}
\\
\end{array}
\right]
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\neg 
\hspace*{2pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em AB}}
\right)
= 
\\
\mathtt{ident}
\left(
\mbox{\em rel2}_{\mbox{\scriptsize\em AB}}
\right)
\\
\end{array}
\\
\wedge 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{source}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em AB}}
\right)
= 
\\
\mathtt{source}
\left(
\mbox{\em rel2}_{\mbox{\scriptsize\em AB}}
\right)
\\
\end{array}
\\
\wedge 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{target}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em AB}}
\right)
= 
\\
\mathtt{target}
\left(
\mbox{\em rel2}_{\mbox{\scriptsize\em AB}}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\]


}

Rule: valid\_childRef\_for\_all\_FE\_relations\_fast\label{rule_generated:valid_childRef_for_all_FE_relations_fast} importance: 150\newline Every Frame Element relation should have a valid (i.e. non-null and existent) source reference. This rule can be evaluated much faster than its corresponding rule in ReulesFERelationSanity.xml because now we use the SQL database to select the appropriate FE and don't look ourselves within all FEs{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFERelations}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{source}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
\right)
\not= 
\hspace*{2pt}
\mathsf{0}
\\
\wedge 
\\
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\neg 
\hspace*{2pt}
\mathtt{source}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
\right)
= 
\hspace*{2pt}
\mathsf{0}
\\
\implies 
\\
\neg 
\hspace*{2pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{null}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{getFEByID}
\left(
\mathtt{fnDB}
,
\mathtt{source}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
\right)
\right)
\\
\end{array}
\right)
\\
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\]


}

Rule: valid\_targetRef\_for\_all\_FE\_relations\_fast\label{rule_generated:valid_targetRef_for_all_FE_relations_fast} importance: 150\newline Every Frame Element relation should have a valid (i.e. non-null and existent) target reference. This rule can be evaluated much faster than its corresponding rule in ReulesFERelationSanity.xml because now we use the SQL database to select the appropriate FE and don't look ourselves within all FEs{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFERelations}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{target}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
\right)
\not= 
\hspace*{2pt}
\mathsf{0}
\\
\wedge 
\\
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\neg 
\hspace*{2pt}
\mathtt{target}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
\right)
= 
\hspace*{2pt}
\mathsf{0}
\\
\implies 
\\
\neg 
\hspace*{2pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{null}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{getFEByID}
\left(
\mathtt{fnDB}
,
\mathtt{target}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
\right)
\right)
\\
\end{array}
\right)
\\
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\]


}

Rule: core\_FEs\_are\_inherited\_if\_not\_in\_coreset\_and\_not\_in\_excludes\label{rule_generated:core_FEs_are_inherited_if_not_in_coreset_and_not_in_excludes} importance: 145\newline All core Frame Elements of a Frame are inherited if they are not part of a coreset or an excludes set of this Frame.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\neg 
\hspace*{2pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\in 
\\
\mathtt{concat}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{getCoreSets}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\\
\end{array}
\\
\\
\end{array}
\\
\wedge 
\\
\neg 
\hspace*{2pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\in 
\\
\mathtt{concat}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{getExcludes}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\\
\end{array}
\\
\\
\end{array}
\\
\wedge 
\\
\mathtt{feType}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\right)
= 
\hspace*{2pt}
\mathtt{Core}
\\
\end{array}
\right)
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{target}
,
\\
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Inheritance}
\\
\end{array}
\right]
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameByID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{source}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
^{
\mathsf{Add}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{frameRelationRef}
,
\\
\mathtt{getAllFERelations}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{target}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
\right)
= 
\\
\mathtt{ident}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\right)
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
. 
\mathtt{target}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\hspace*{3pt}
10
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\wedge 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{source}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
\right)
= 
\\
\mathtt{ident}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\right)
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
. 
\mathtt{source}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
\hspace*{3pt}
10
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: coreset\_FEs\_are\_inherited\label{rule_generated:coreset_FEs_are_inherited} importance: 145\newline At least one Frame Element of each coreset of a Frame is inherited.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em coreset}_{\mbox{\scriptsize\em parent}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getCoreSets}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Chg}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mbox{\em coreset}_{\mbox{\scriptsize\em parent}}
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{target}
,
\\
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Inheritance}
\\
\end{array}
\right]
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameByID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{source}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
^{
\mathsf{Add}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{frameRelationRef}
,
\\
\mathtt{getAllFERelations}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{target}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
\right)
= 
\\
\mathtt{ident}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\right)
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
. 
\mathtt{target}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\hspace*{3pt}
10
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\wedge 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{source}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
\right)
= 
\\
\mathtt{ident}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\right)
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
. 
\mathtt{source}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
\hspace*{3pt}
10
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: excluding\_FEs\_are\_inherited\_if\_one\_core\label{rule_generated:excluding_FEs_are_inherited_if_one_core} importance: 145\newline Of two mutually excluding FEs of a Frame either both are not core or at least one of them is core and inherited.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em excludes}_{\mbox{\scriptsize\em parent}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getExcludes}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em parent}_{\mbox{\scriptsize\em non}_{\mbox{\scriptsize\em core}}}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mbox{\em excludes}_{\mbox{\scriptsize\em parent}}
\hspace*{5pt}
\bullet 
\\
\neg 
\hspace*{2pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em parent}_{\mbox{\scriptsize\em non}_{\mbox{\scriptsize\em core}}}}
\right)
= 
\\
\mathtt{Core}
\\
\end{array}
\\
\\
\end{array}
\\
\end{array}
\right)
\\
\vee 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Chg}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mbox{\em excludes}_{\mbox{\scriptsize\em parent}}
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\right)
= 
\\
\mathtt{Core}
\\
\end{array}
\left\{
\left\{
\right\}
\right\}
\\
\wedge 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{target}
,
\\
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Inheritance}
\\
\end{array}
\right]
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameByID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{source}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
^{
\mathsf{Add}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{frameRelationRef}
,
\\
\mathtt{getAllFERelations}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{target}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
\right)
= 
\\
\mathtt{ident}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\right)
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
. 
\mathtt{target}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\hspace*{3pt}
10
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\wedge 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{source}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
\right)
= 
\\
\mathtt{ident}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\right)
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
. 
\mathtt{source}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
\hspace*{3pt}
10
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: inheritance\_FE\_property\_coreset\_inherited\_reverse\label{rule_generated:inheritance_FE_property_coreset_inherited_reverse} importance: 140\newline The coreset property of frame elements propagated up the inheritance relation, i.e.: Each frame element in a coreset must have at least one corresponding frame element in the parent frame. All these parent frame elements must be part of one coreset of the parent frame.
This rule is necessary from the logic point of view, saying that the child frame is more specific than the parent frame (you must not introduce new frame elements into a core set because this would open the semantic space of the child frame instead of narrowing it).
That means that the restrictions of the child frame must imply the restricions of the parent frame.
Frame elements in the coreset are logically connected via "or" whereas all other (except for extrathematic) frame elements are logically connected via "and".
So for two frame elements a and b the rule says that if we have "a or b" in the child frame we cannot have "a and b" in the parent frame.
{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em coreset}_{\mbox{\scriptsize\em child}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getCoreSets}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{source}
,
\\
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Inheritance}
\\
\end{array}
\right]
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameByID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{target}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em mappings}_{\mbox{\scriptsize\em coreset}}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em coreset}_{\mbox{\scriptsize\em child}}
,
\\
\mathtt{fst}
,
\\
\mathtt{getFEMappings}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\\
\end{array}
\right]
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\neg 
\hspace*{2pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{null}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em mappings}_{\mbox{\scriptsize\em coreset}}}
\\
\end{array}
\right)
\\
\\
\end{array}
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em coreset}_{\mbox{\scriptsize\em child}}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mbox{\em coreset}_{\mbox{\scriptsize\em child}}
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em mapping}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em mappings}_{\mbox{\scriptsize\em coreset}}}
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em coreset}_{\mbox{\scriptsize\em child}}}
= 
\\
\mathtt{fst}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em mapping}}
\right)
\\
\end{array}
\\
\\
\end{array}
\\
\end{array}
\\
\end{array}
\right)
\\
\wedge 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em coreset}_{\mbox{\scriptsize\em parent}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getCoreSets}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{map}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{snd}
,
\\
\mbox{\em fe}_{\mbox{\scriptsize\em mappings}_{\mbox{\scriptsize\em coreset}}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\in 
\\
\mbox{\em coreset}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: inheritance\_FE\_property\_excludes\_inherited\_reverse\label{rule_generated:inheritance_FE_property_excludes_inherited_reverse} importance: 140\newline The excludes property of frame elements propageted upwards the inheritance relation, i.e.: For each frame element f1 excluding another FE f2 of the child frame we determine the corresponding frame elements f1' and f2' in the parent frame. If both exist then they also should exclude each other.
This rule is necessary from the logic point of view, saying that the child frame is more specific than the parent frame.
That means that the restrictions of the child frame must imply the restricions of the parent frame.
Frame elements that exclude each other are logically connected via "xor" whereas all other (except for extrathematic) frame elements are logically connected via "and".
So for two frame elements a and b the rule says that if we have "a xor b" in the child frame we cannot have "a and b" in the parent frame.
{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em excl}_{\mbox{\scriptsize\em child}}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getExcludes}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{source}
,
\\
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Inheritance}
\\
\end{array}
\right]
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameByID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{target}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em mappings}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em excl}}}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em excl}_{\mbox{\scriptsize\em child}}}
,
\\
\mathtt{fst}
,
\\
\mathtt{getFEMappings}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\\
\end{array}
\right]
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{length}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em mappings}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em excl}}}}
\right)
\mathtt{>=}
\\
\mathsf{2}
\\
\end{array}
\\
\\
\end{array}
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em excl}_{\mbox{\scriptsize\em parent}}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getExcludes}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{map}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{snd}
,
\\
\mbox{\em fe}_{\mbox{\scriptsize\em mappings}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em excl}}}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\in 
\\
\mbox{\em fe}_{\mbox{\scriptsize\em excl}_{\mbox{\scriptsize\em parent}}}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: inheritance\_FE\_property\_requires\_inherited\_reverse\label{rule_generated:inheritance_FE_property_requires_inherited_reverse} importance: 140\newline The requires property of frame elements is propagated upwards, i.e.: For each frame element f1 requiring another FE f2 of the child frame we determine the corresponding frame elements f1' and f2' in the parent frame. If both exist then they also should require each other.
This rule is necessary from the logic point of view, saying that the child frame is more specific than the parent frame.
That means that the restrictions of the child frame must imply the restricions of the parent frame.
Frame elements that require each other are logically connected via "implies" whereas all other (except for extrathematic) frame elements are logically connected via "and".
So for two frame elements a and b the rule says that if we have "a implies b" in the child frame we cannot have "a and b" in the parent frame.
{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em requ}_{\mbox{\scriptsize\em child}}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getRequires}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{source}
,
\\
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Inheritance}
\\
\end{array}
\right]
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameByID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{target}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em mappings}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em requ}}}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em requ}_{\mbox{\scriptsize\em child}}}
,
\\
\mathtt{fst}
,
\\
\mathtt{getFEMappings}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\\
\end{array}
\right]
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{length}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em mappings}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em requ}}}}
\right)
\mathtt{>=}
\\
\mathsf{2}
\\
\end{array}
\\
\\
\end{array}
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em requ}_{\mbox{\scriptsize\em parent}}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getRequires}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{map}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{snd}
,
\\
\mbox{\em fe}_{\mbox{\scriptsize\em mappings}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em requ}}}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\in 
\\
\mbox{\em fe}_{\mbox{\scriptsize\em requ}_{\mbox{\scriptsize\em parent}}}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: inheritance\_mapped\_FEs\_extrathematic\label{rule_generated:inheritance_mapped_FEs_extrathematic} importance: 140\newline Inherited Frame Elements should not change the coreness type from non-extrathematic to extrathematic.
This rule is comprised by inheritance\_mapped\_FEs\_same\_type but it is much more important.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{target}
,
\\
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Inheritance}
\\
\end{array}
\right]
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameByID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{source}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fechild-feparent}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEMappings}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mathtt{fst}
\left(
\mbox{\em fechild-feparent}
\right)
\right)
= 
\\
\mathtt{ExtraThematic}
\\
\end{array}
\\
\\
\end{array}
\\
\implies 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mathtt{snd}
\left(
\mbox{\em fechild-feparent}
\right)
\right)
= 
\\
\mathtt{ExtraThematic}
\\
\end{array}
\\
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: inheritance\_FE\_property\_requires\_inherited\label{rule_generated:inheritance_FE_property_requires_inherited} importance: 138\newline The requires property of frame elements is inherited, i.e.: For each frame element f1 requiring another FE f2 of the parent frame we determine the corresponding frame elements f1' and f2' in the child frame. If both exist then they also should require each other or there is no frame element relation between them (which means that f1' and f2' are both(!) necessary).
This rule is nice to have from the linguistic point of view but not really necessary from the logic point of view (i.e., that the restrictions of the child frame should imply the restrictions of the parent frame).
{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em requ}_{\mbox{\scriptsize\em parent}}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getRequires}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{target}
,
\\
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Inheritance}
\\
\end{array}
\right]
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameByID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{source}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em mappings}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em requ}}}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em requ}_{\mbox{\scriptsize\em parent}}}
,
\\
\mathtt{snd}
,
\\
\mathtt{getFEMappings}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\\
\end{array}
\right]
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{length}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em mappings}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em requ}}}}
\right)
\mathtt{>=}
\\
\mathsf{2}
\\
\end{array}
\\
\\
\end{array}
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left(
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em requ}_{\mbox{\scriptsize\em child}}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getRequires}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{map}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fst}
,
\\
\mbox{\em fe}_{\mbox{\scriptsize\em mappings}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em requ}}}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\in 
\\
\mbox{\em fe}_{\mbox{\scriptsize\em requ}_{\mbox{\scriptsize\em child}}}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\right)
\\
\vee 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em conn}_{\mbox{\scriptsize\em child}}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{getRequires}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
+\hspace{-1pt}+ 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{getCoreSets}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
+\hspace{-1pt}+ 
\\
\mathtt{getExcludes}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em child2}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{map}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fst}
,
\\
\mbox{\em fe}_{\mbox{\scriptsize\em mappings}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em requ}}}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\neg 
\hspace*{2pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em child2}}
\in 
\\
\mbox{\em fe}_{\mbox{\scriptsize\em conn}_{\mbox{\scriptsize\em child}}}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: frame\_elements\_same\_name\_mapped\_for\_inheritance\_using\_causativeof\_inchaoativeof\_subframe\_perspective\_on\label{rule_generated:frame_elements_same_name_mapped_for_inheritance_using_causativeof_inchaoativeof_subframe_perspective_on} importance: 135\newline If two Frames are related (by inheritance, using, causative of, inchoative of, subframe perspective of relation) then those Frame Elements having the same names should be mapped.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{target}
,
\\
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Inheritance}
,
\\
\mathsf{Using}
,
\\
\mathsf{Causative}_{\mbox{\scriptsize\em of}}
,
\\
\mathsf{Inchoative}_{\mbox{\scriptsize\em of}}
,
\\
\mathsf{Subframe}
,
\\
\mathsf{Perspective}_{\mbox{\scriptsize\em on}}
\\
\end{array}
\right]
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameByID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{source}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{name}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\right)
= 
\\
\mathtt{name}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\right)
\\
\end{array}
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
^{
\mathsf{Add}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{frameRelationRef}
,
\\
\mathtt{getAllFERelations}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{source}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
\right)
= 
\\
\mathtt{ident}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\right)
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
. 
\mathtt{source}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
\hspace*{3pt}
2
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\wedge 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{target}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
\right)
= 
\\
\mathtt{ident}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\right)
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
. 
\mathtt{target}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\hspace*{3pt}
2
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: inheritance\_FE\_property\_excludes\_inherited\label{rule_generated:inheritance_FE_property_excludes_inherited} importance: 135\newline The excludes property of frame elements is inherited, i.e.: For each frame element f1 excluding another FE f2 of the parent frame we determine the corresponding frame elements f1' and f2' in the child frame. If both exist then they also should exclude each other.
This rule is nice to have from the linguistic point of view but not really necessary from the logic point of view (i.e., that the restrictions of the child frame should imply the restrictions of the parent frame).{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em excl}_{\mbox{\scriptsize\em parent}}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getExcludes}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{target}
,
\\
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Inheritance}
\\
\end{array}
\right]
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameByID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{source}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em mappings}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em excl}}}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em excl}_{\mbox{\scriptsize\em parent}}}
,
\\
\mathtt{snd}
,
\\
\mathtt{getFEMappings}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\\
\end{array}
\right]
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{length}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em mappings}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em excl}}}}
\right)
\mathtt{>=}
\\
\mathsf{2}
\\
\end{array}
\\
\\
\end{array}
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em excl}_{\mbox{\scriptsize\em child}}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getExcludes}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{map}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fst}
,
\\
\mbox{\em fe}_{\mbox{\scriptsize\em mappings}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em excl}}}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\in 
\\
\mbox{\em fe}_{\mbox{\scriptsize\em excl}_{\mbox{\scriptsize\em child}}}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: inheritance\_FE\_property\_coreset\_inherited\label{rule_generated:inheritance_FE_property_coreset_inherited} importance: 130\newline The coreset property of frame elements is inherited, i.e.: For each frame element in a coreset of the parent frame we determine the corresponding frame elements in the child frame. If there are at least 2 then these must be part of a coreset of the child frame.
This rule is nice to have from the linguistic point of view but not really necessary from the logic point of view (i.e., that the restrictions of the child frame should imply the restrictions of the parent frame).{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em coreset}_{\mbox{\scriptsize\em parent}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getCoreSets}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{target}
,
\\
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Inheritance}
\\
\end{array}
\right]
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameByID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{source}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em mappings}_{\mbox{\scriptsize\em coreset}}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em coreset}_{\mbox{\scriptsize\em parent}}
,
\\
\mathtt{snd}
,
\\
\mathtt{getFEMappings}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\\
\end{array}
\right]
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{length}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em mappings}_{\mbox{\scriptsize\em coreset}}}
\right)
\mathtt{>=}
\\
\mathsf{2}
\\
\end{array}
\\
\\
\end{array}
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em coreset}_{\mbox{\scriptsize\em child}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getCoreSets}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{map}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fst}
,
\\
\mbox{\em fe}_{\mbox{\scriptsize\em mappings}_{\mbox{\scriptsize\em coreset}}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\in 
\\
\mbox{\em coreset}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: inheritance\_all\_frame\_STs\_are\_inherited\label{rule_generated:inheritance_all_frame_STs_are_inherited} importance: 130\newline All semantic types of a parent frame (except the "Non ..." types) are inherited to all child frames.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em st}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameSTs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\neg 
\hspace*{2pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Non}
= 
\\
\mathtt{takeS}
\left(
\mathsf{3}
,
\mathtt{name}
\left(
\mbox{\em st}_{\mbox{\scriptsize\em parent}}
\right)
\right)
\\
\end{array}
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{target}
,
\\
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Inheritance}
\\
\end{array}
\right]
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameByID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{source}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em st}_{\mbox{\scriptsize\em child}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameSTs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em st}_{\mbox{\scriptsize\em sub}_{\mbox{\scriptsize\em parent}}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em st}_{\mbox{\scriptsize\em parent}}
,
\\
\mathtt{getSubSTs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em st}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\\
\end{array}
\right]
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em st}_{\mbox{\scriptsize\em child}}
= 
\hspace*{2pt}
\mbox{\em st}_{\mbox{\scriptsize\em sub}_{\mbox{\scriptsize\em parent}}}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em st}_{\mbox{\scriptsize\em child}}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mbox{\em st}_{\mbox{\scriptsize\em sub}_{\mbox{\scriptsize\em parent}}}
\hspace*{3pt}
2
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: inheritance\_mapped\_FEs\_same\_type\label{rule_generated:inheritance_mapped_FEs_same_type} importance: 130\newline The Frame Elements that are mapped to each other as part of an inheritance relation should have the same type.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{target}
,
\\
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Inheritance}
\\
\end{array}
\right]
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameByID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{source}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fechild-feparent}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEMappings}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mathtt{fst}
\left(
\mbox{\em fechild-feparent}
\right)
\right)
= 
\\
\mathtt{feType}
\left(
\mathtt{snd}
\left(
\mbox{\em fechild-feparent}
\right)
\right)
\\
\end{array}
\\
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: semantictypes\_of\_mapped\_FEs\_are\_inherited\_inheritance\_relation\label{rule_generated:semantictypes_of_mapped_FEs_are_inherited_inheritance_relation} importance: 130\newline All semantic types of an FE are inherited if it is mapped to another FE as part of an inheritance relation.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{target}
,
\\
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Inheritance}
\\
\end{array}
\right]
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameByID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{source}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fechild-feparent}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEMappings}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em st}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em parent}}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFESTs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{snd}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fechild-feparent}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em st}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em child}}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFESTs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{fst}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fechild-feparent}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em st}_{\mbox{\scriptsize\em sub}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em parent}}}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em st}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em parent}}}
,
\\
\mathtt{getSubSTs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em st}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em parent}}}
\\
\end{array}
\right)
\\
\end{array}
\right]
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em st}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em child}}}
= 
\\
\mbox{\em st}_{\mbox{\scriptsize\em sub}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em parent}}}}
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em st}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em child}}}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mbox{\em st}_{\mbox{\scriptsize\em sub}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em parent}}}}
\hspace*{3pt}
2
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: inchoative-of\_all\_core\_FEs\_mapped\label{rule_generated:inchoative-of_all_core_FEs_mapped} importance: 125\newline For an Inchoative\\_of relation, each core (or core-unexpressed) FE of the parent Frame should be mapped to a FE of the child Frame.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em inch}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{target}
,
\\
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Inchoative}_{\mbox{\scriptsize\em of}}
\\
\end{array}
\right]
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\right)
= 
\\
\mathtt{Core}
\\
\end{array}
\\
\vee 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\right)
= 
\\
\mathtt{CoreUnexpressed}
\\
\end{array}
\\
\end{array}
\right)
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameByID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{source}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em inch}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
^{
\mathsf{Add}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em inch}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{frameRelationRef}
,
\\
\mathtt{getAllFERelations}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{target}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
\right)
= 
\\
\mathtt{ident}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\right)
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
. 
\mathtt{target}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\hspace*{3pt}
2
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\wedge 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{source}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
\right)
= 
\\
\mathtt{ident}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\right)
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
. 
\mathtt{source}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
\hspace*{3pt}
2
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: causative-of\_all\_core\_FEs\_mapped\_except\_Agent\_Cause\label{rule_generated:causative-of_all_core_FEs_mapped_except_Agent_Cause} importance: 120\newline For an Causative\\_of relation, each core (or core-unexpressed) FE (except perhaps Agent or Cause) of the parent Frame should be mapped to a FE of the child Frame.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em caus}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{target}
,
\\
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Causative}_{\mbox{\scriptsize\em of}}
\\
\end{array}
\right]
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\right)
= 
\\
\mathtt{Core}
\\
\end{array}
\\
\\
\end{array}
\\
\vee 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\right)
= 
\\
\mathtt{CoreUnexpressed}
\\
\end{array}
\\
\\
\end{array}
\\
\end{array}
\right)
\\
\wedge 
\\
\neg 
\hspace*{2pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{name}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\right)
= 
\\
\mathsf{Agent}
\\
\end{array}
\\
\wedge 
\\
\neg 
\hspace*{2pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{name}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\right)
= 
\\
\mathsf{Cause}
\\
\end{array}
\\
\end{array}
\right)
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameByID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{source}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em caus}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
^{
\mathsf{Add}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em caus}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{frameRelationRef}
,
\\
\mathtt{getAllFERelations}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{target}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
\right)
= 
\\
\mathtt{ident}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\right)
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
. 
\mathtt{target}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\hspace*{3pt}
2
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\wedge 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{source}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
\right)
= 
\\
\mathtt{ident}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\right)
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
. 
\mathtt{source}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
\hspace*{3pt}
2
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: perspective\_on\_one\_core\_FEs\_is\_mapped\label{rule_generated:perspective_on_one_core_FEs_is_mapped} importance: 115\newline For a Perspective\_on relation, one core (or core-unexpressed) FE of the parent Frame should be mapped to a FE of the child Frame.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em pers}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{target}
,
\\
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Perspective}_{\mbox{\scriptsize\em on}}
\\
\end{array}
\right]
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\right)
= 
\\
\mathtt{Core}
\\
\end{array}
\\
\vee 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\right)
= 
\\
\mathtt{CoreUnexpressed}
\\
\end{array}
\\
\end{array}
\right)
\\
\wedge 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameByID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{source}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em pers}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
^{
\mathsf{Add}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em pers}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{frameRelationRef}
,
\\
\mathtt{getAllFERelations}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{target}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
\right)
= 
\\
\mathtt{ident}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\right)
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
. 
\mathtt{target}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\hspace*{3pt}
10
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\wedge 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{source}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
\right)
= 
\\
\mathtt{ident}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\right)
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
. 
\mathtt{source}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
\hspace*{3pt}
10
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: subframe\_no\_other\_relations\label{rule_generated:subframe_no_other_relations} importance: 115\newline If Frames A and B point to a common Frame C via Subframe then A and B should not be connected at all except by the precedence relation. At the moment the precedence relation is a META relation, not expressed in the Relation Table, which might change in the future. Then, we have to use filterNotElem in order to get all Frame-to-Frame relations except Precedence...{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em AC}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameRelationsByType}
\left(
\mathtt{fnDB}
,
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Subframe}
\\
\end{array}
\right]
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em BC}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameRelationsByType}
\left(
\mathtt{fnDB}
,
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Subframe}
\\
\end{array}
\right]
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{target}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em AC}}
\right)
= 
\hspace*{2pt}
\mathtt{target}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em BC}}
\right)
\\
\implies 
\\
\neg 
\hspace*{2pt}
\left(
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em AB}}
^{
\mathsf{Del}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrameRelations}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{source}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em AB}}
\right)
= 
\\
\mathtt{source}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em AC}}
\right)
\\
\end{array}
\\
\wedge 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{target}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em AB}}
\right)
= 
\\
\mathtt{source}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em BC}}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: subframe\_one\_core\_FEs\_mapped\label{rule_generated:subframe_one_core_FEs_mapped} importance: 115\newline For a Subframe relation, one core (or core-unexpressed) FE of the parent Frame should be mapped to a FE of the child Frame.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em sub}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{target}
,
\\
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Subframe}
\\
\end{array}
\right]
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\right)
= 
\\
\mathtt{CoreUnexpressed}
\\
\end{array}
\\
\vee 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\right)
= 
\\
\mathtt{Core}
\\
\end{array}
\\
\end{array}
\right)
\\
\wedge 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameByID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{source}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em sub}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
^{
\mathsf{Add}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em sub}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{frameRelationRef}
,
\\
\mathtt{getAllFERelations}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{target}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
\right)
= 
\\
\mathtt{ident}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\right)
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
. 
\mathtt{target}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\hspace*{3pt}
2
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\wedge 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{source}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
\right)
= 
\\
\mathtt{ident}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\right)
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
. 
\mathtt{source}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
\hspace*{3pt}
2
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: using\_one\_core\_FEs\_is\_mapped\label{rule_generated:using_one_core_FEs_is_mapped} importance: 115\newline For a Using relation, one core (or core-unexpressed) FE of the parent Frame should be mapped to a FE of the child Frame.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em using}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{target}
,
\\
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Using}
\\
\end{array}
\right]
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\right)
= 
\\
\mathtt{Core}
\\
\end{array}
\\
\vee 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\right)
= 
\\
\mathtt{CoreUnexpressed}
\\
\end{array}
\\
\end{array}
\right)
\\
\wedge 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameByID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{source}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em using}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
^{
\mathsf{Add}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em using}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{frameRelationRef}
,
\\
\mathtt{getAllFERelations}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{target}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
\right)
= 
\\
\mathtt{ident}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\right)
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
. 
\mathtt{target}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\hspace*{3pt}
10
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\wedge 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{source}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
\right)
= 
\\
\mathtt{ident}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\right)
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em rel}_{\mbox{\scriptsize\em fe}}
. 
\mathtt{source}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
\hspace*{3pt}
10
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: subframe\_precedes\_same\_subframe\label{rule_generated:subframe_precedes_same_subframe} importance: 114\newline If Frames A and B are connected via a precedes relation then they must be subframes of a common Frame C.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em prec}_{\mbox{\scriptsize\em AB}}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Precedes}
\\
\end{array}
\right]
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em sub}_{\mbox{\scriptsize\em AC}}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameRelationsByType}
\left(
\mathtt{fnDB}
,
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Subframe}
\\
\end{array}
\right]
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em sub}_{\mbox{\scriptsize\em BC}}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameRelationsByType}
\left(
\mathtt{fnDB}
,
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Subframe}
\\
\end{array}
\right]
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{source}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em prec}_{\mbox{\scriptsize\em AB}}}
\right)
= 
\\
\mathtt{source}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em sub}_{\mbox{\scriptsize\em AC}}}
\right)
\\
\end{array}
\\
\wedge 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{target}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em prec}_{\mbox{\scriptsize\em AB}}}
\right)
= 
\\
\mathtt{source}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em sub}_{\mbox{\scriptsize\em BC}}}
\right)
\\
\end{array}
\\
\wedge 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{target}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em sub}_{\mbox{\scriptsize\em AC}}}
\right)
= 
\\
\mathtt{target}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em sub}_{\mbox{\scriptsize\em BC}}}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: perspective\_on\_all\_frame\_STs\_are\_inherited\label{rule_generated:perspective_on_all_frame_STs_are_inherited} importance: 110\newline All semantic types of a parent frame are inherited to all child frames that use the parent Frame.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em st}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameSTs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\neg 
\hspace*{2pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Non}
= 
\\
\mathtt{takeS}
\left(
\mathsf{3}
,
\mathtt{name}
\left(
\mbox{\em st}_{\mbox{\scriptsize\em parent}}
\right)
\right)
\\
\end{array}
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em pers}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{target}
,
\\
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Perspective}_{\mbox{\scriptsize\em on}}
\\
\end{array}
\right]
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameByID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{source}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em pers}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em st}_{\mbox{\scriptsize\em child}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameSTs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em st}_{\mbox{\scriptsize\em sub}_{\mbox{\scriptsize\em parent}}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em st}_{\mbox{\scriptsize\em parent}}
,
\\
\mathtt{getSubSTs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em st}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\\
\end{array}
\right]
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em st}_{\mbox{\scriptsize\em child}}
= 
\hspace*{2pt}
\mbox{\em st}_{\mbox{\scriptsize\em sub}_{\mbox{\scriptsize\em parent}}}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em st}_{\mbox{\scriptsize\em child}}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mbox{\em st}_{\mbox{\scriptsize\em sub}_{\mbox{\scriptsize\em parent}}}
\hspace*{3pt}
2
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: perspective\_on\_mapped\_FEs\_same\_type\label{rule_generated:perspective_on_mapped_FEs_same_type} importance: 110\newline The Frame Elements that are mapped to each other as part of a Perspective\_on relation should have the same type.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em pers}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{target}
,
\\
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Perspective}_{\mbox{\scriptsize\em on}}
\\
\end{array}
\right]
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameByID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{source}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em pers}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fechild-feparent}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEMappings}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em rel}_{\mbox{\scriptsize\em pers}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mathtt{fst}
\left(
\mbox{\em fechild-feparent}
\right)
\right)
= 
\\
\mathtt{feType}
\left(
\mathtt{snd}
\left(
\mbox{\em fechild-feparent}
\right)
\right)
\\
\end{array}
\\
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: semantictypes\_of\_mapped\_FEs\_are\_inherited\_perspective\_on\_relation\label{rule_generated:semantictypes_of_mapped_FEs_are_inherited_perspective_on_relation} importance: 110\newline All semantic types of an FE are inherited if it is mapped to another FE as part of an perspective\_on relation.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em pers}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{target}
,
\\
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Perspective}_{\mbox{\scriptsize\em on}}
\\
\end{array}
\right]
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameByID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{source}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em pers}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fechild-feparent}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEMappings}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em rel}_{\mbox{\scriptsize\em pers}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em st}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em parent}}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFESTs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{snd}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fechild-feparent}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em st}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em child}}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFESTs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{fst}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fechild-feparent}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em st}_{\mbox{\scriptsize\em sub}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em parent}}}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em st}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em parent}}}
,
\\
\mathtt{getSubSTs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em st}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em parent}}}
\\
\end{array}
\right)
\\
\end{array}
\right]
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em st}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em child}}}
= 
\\
\mbox{\em st}_{\mbox{\scriptsize\em sub}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em parent}}}}
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em st}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em child}}}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mbox{\em st}_{\mbox{\scriptsize\em sub}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em parent}}}}
\hspace*{3pt}
2
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: semantictypes\_of\_mapped\_FEs\_are\_inherited\_using\_relation\label{rule_generated:semantictypes_of_mapped_FEs_are_inherited_using_relation} importance: 110\newline All semantic types of an FE are inherited if it is mapped to another FE as part of an using relation.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em using}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{target}
,
\\
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Using}
\\
\end{array}
\right]
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameByID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{source}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em using}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fechild-feparent}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEMappings}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em rel}_{\mbox{\scriptsize\em using}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em st}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em parent}}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFESTs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{snd}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fechild-feparent}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em st}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em child}}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFESTs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{fst}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fechild-feparent}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em st}_{\mbox{\scriptsize\em sub}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em parent}}}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em st}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em parent}}}
,
\\
\mathtt{getSubSTs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em st}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em parent}}}
\\
\end{array}
\right)
\\
\end{array}
\right]
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em st}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em child}}}
= 
\\
\mbox{\em st}_{\mbox{\scriptsize\em sub}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em parent}}}}
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em st}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em child}}}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mbox{\em st}_{\mbox{\scriptsize\em sub}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em parent}}}}
\hspace*{3pt}
2
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: using\_all\_frame\_STs\_are\_inherited\label{rule_generated:using_all_frame_STs_are_inherited} importance: 110\newline All semantic types of a parent frame are inherited to all child frames that use the parent Frame.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em st}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameSTs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\neg 
\hspace*{2pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Non}
= 
\\
\mathtt{takeS}
\left(
\mathsf{3}
,
\mathtt{name}
\left(
\mbox{\em st}_{\mbox{\scriptsize\em parent}}
\right)
\right)
\\
\end{array}
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em using}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{target}
,
\\
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Using}
\\
\end{array}
\right]
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameByID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{source}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em using}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em st}_{\mbox{\scriptsize\em child}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameSTs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em st}_{\mbox{\scriptsize\em sub}_{\mbox{\scriptsize\em parent}}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em st}_{\mbox{\scriptsize\em parent}}
,
\\
\mathtt{getSubSTs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em st}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\\
\end{array}
\right]
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em st}_{\mbox{\scriptsize\em child}}
= 
\hspace*{2pt}
\mbox{\em st}_{\mbox{\scriptsize\em sub}_{\mbox{\scriptsize\em parent}}}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em st}_{\mbox{\scriptsize\em child}}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mbox{\em st}_{\mbox{\scriptsize\em sub}_{\mbox{\scriptsize\em parent}}}
\hspace*{3pt}
2
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: using\_mapped\_FEs\_same\_type\label{rule_generated:using_mapped_FEs_same_type} importance: 110\newline The Frame Elements that are mapped to each other as part of a Using relation should have the same type.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em using}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{target}
,
\\
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Using}
\\
\end{array}
\right]
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameByID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{source}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em using}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fechild-feparent}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEMappings}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em rel}_{\mbox{\scriptsize\em using}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mathtt{fst}
\left(
\mbox{\em fechild-feparent}
\right)
\right)
= 
\\
\mathtt{feType}
\left(
\mathtt{snd}
\left(
\mbox{\em fechild-feparent}
\right)
\right)
\\
\end{array}
\\
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: seealso\_one\_representative\label{rule_generated:seealso_one_representative} importance: 100\newline If Frames A and B point to a common Frame C via Seealso then A and B should not be connected by Seealso.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em AC}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameRelationsByType}
\left(
\mathtt{fnDB}
,
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{See}_{\mbox{\scriptsize\em also}}
\\
\end{array}
\right]
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em BC}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameRelationsByType}
\left(
\mathtt{fnDB}
,
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{See}_{\mbox{\scriptsize\em also}}
\\
\end{array}
\right]
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{target}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em AC}}
\right)
= 
\hspace*{2pt}
\mathtt{target}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em BC}}
\right)
\\
\implies 
\\
\neg 
\hspace*{2pt}
\left(
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em AB}}
^{
\mathsf{Del}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{See}_{\mbox{\scriptsize\em also}}
\\
\end{array}
\right]
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{source}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em AB}}
\right)
= 
\\
\mathtt{source}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em AC}}
\right)
\\
\end{array}
\\
\wedge 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{target}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em AB}}
\right)
= 
\\
\mathtt{source}
\left(
\mbox{\em rel}_{\mbox{\scriptsize\em BC}}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: semantictypes\_of\_LUs\_correspond\_to\_STs\_of\_frames\label{rule_generated:semantictypes_of_LUs_correspond_to_STs_of_frames} importance: 70\newline For each Frame we require that all of its semantic types are respected by all its LUs{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em st}_{\mbox{\scriptsize\em frame}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameSTs}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em lu}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getLUs}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em st}_{\mbox{\scriptsize\em lu}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getLUSTs}
\left(
\mathtt{fnDB}
,
\mbox{\em lu}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em st}_{\mbox{\scriptsize\em sub}_{\mbox{\scriptsize\em frame}}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em st}_{\mbox{\scriptsize\em frame}}
,
\\
\mathtt{getSubSTs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em st}_{\mbox{\scriptsize\em frame}}
\\
\end{array}
\right)
\\
\end{array}
\right]
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em st}_{\mbox{\scriptsize\em lu}}
= 
\hspace*{2pt}
\mbox{\em st}_{\mbox{\scriptsize\em sub}_{\mbox{\scriptsize\em frame}}}
\\
\left\{
\left\{
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em st}_{\mbox{\scriptsize\em lu}}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mbox{\em st}_{\mbox{\scriptsize\em sub}_{\mbox{\scriptsize\em frame}}}
\hspace*{3pt}
2
\right\}
\right\}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: lemmas\_multiple\_lexentries\_exactly\_one\_head\_and\_equal\_part\_of\_spch\label{rule_generated:lemmas_multiple_lexentries_exactly_one_head_and_equal_part_of_spch} importance: 65\newline For each Lemma connected to a LU we require that if it has multiple LexemeEntries then it exactly one of them is the head word and the part of speech of its associated Lexeme is the same as the part of speech of the Lemma.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em lemma}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllLemmas}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\neg 
\hspace*{2pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{null}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{getLemmaLUs}
\left(
\mathtt{fnDB}
,
\mbox{\em lemma}
\right)
\\
\end{array}
\right)
\\
\\
\end{array}
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em lexentries}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{getLemmaLexEntries}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em lemma}
\\
\end{array}
\right)
\\
\end{array}
\right]
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{length}
\left(
\mbox{\em lexentries}
\right)
\mathtt{>}
\hspace*{2pt}
\mathsf{1}
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em lexentries}_{\mbox{\scriptsize\em headword}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{filter}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{headWord}
,
\\
\mbox{\em lexentries}
\\
\end{array}
\right)
\\
\end{array}
\right]
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{length}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em lexentries}_{\mbox{\scriptsize\em headword}}
\\
\end{array}
\right)
= 
\\
\mathsf{1}
\\
\end{array}
\\
\\
\end{array}
\\
\wedge 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em lexentry}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mbox{\em lexentries}_{\mbox{\scriptsize\em headword}}
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{lemmaPartOfSpchRef}
\left(
\mbox{\em lexentry}
\right)
= 
\\
\mathtt{lexemePartOfSpchRef}
\left(
\mbox{\em lexentry}
\right)
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em lexentry}
. 
\mathtt{lemmaPartOfSpchRef}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{lexemePartOfSpchRef}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em lexentry}
\\
\end{array}
\right)
\hspace*{3pt}
\\
\end{array}
\right\}
,
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em lexentry}
. 
\mathtt{lexemePartOfSpchRef}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{lemmaPartOfSpchRef}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em lexentry}
\\
\end{array}
\right)
\hspace*{3pt}
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\]


}

Rule: lemmas\_one\_lexentry\_same\_POS\label{rule_generated:lemmas_one_lexentry_same_POS} importance: 65\newline For each Lemma connected to a LU we require that if it has only one LexemeEntry then the part of speech of the associated Lexeme is the same as the part of speech of the Lemma.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em lemma}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllLemmas}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\neg 
\hspace*{2pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{null}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{getLemmaLUs}
\left(
\mathtt{fnDB}
,
\mbox{\em lemma}
\right)
\\
\end{array}
\right)
\\
\\
\end{array}
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em lexentries}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{getLemmaLexEntries}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em lemma}
\\
\end{array}
\right)
\\
\end{array}
\right]
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{length}
\left(
\mbox{\em lexentries}
\right)
= 
\hspace*{2pt}
\mathsf{1}
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em lexentry}
^{
\mathsf{Chg}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mbox{\em lexentries}
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{lemmaPartOfSpchRef}
\left(
\mbox{\em lexentry}
\right)
= 
\\
\mathtt{lexemePartOfSpchRef}
\left(
\mbox{\em lexentry}
\right)
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em lexentry}
. 
\mathtt{lemmaPartOfSpchRef}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{lexemePartOfSpchRef}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em lexentry}
\\
\end{array}
\right)
\hspace*{3pt}
\\
\end{array}
\right\}
,
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em lexentry}
. 
\mathtt{lexemePartOfSpchRef}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{lemmaPartOfSpchRef}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em lexentry}
\\
\end{array}
\right)
\hspace*{3pt}
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\]


}

Rule: lexUnit\_description\_proper\label{rule_generated:lexUnit_description_proper} importance: 60\newline We require that the descriptions of LUs start either with FN: or COD:.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em lu}
^{
\mathsf{Chg}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllLUs}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{isPrefixOfS}
\left(
\mathsf{FN:}
,
\mathtt{description}
\left(
\mbox{\em lu}
\right)
\right)
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em lu}
. 
\mathtt{description}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{mkProperLUDesc}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{description}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em lu}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{3pt}
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\vee 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{isPrefixOfS}
\left(
\mathsf{COD:}
,
\mathtt{description}
\left(
\mbox{\em lu}
\right)
\right)
\\
\left\{
\left\{
\right\}
\right\}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: frames\_fes\_name\_abbrev\_unique\label{rule_generated:frames_fes_name_abbrev_unique} importance: 49\newline Within each Frame the Names and Abbreviations of each Frame Element are unique (necessary for referencing them in the XML definitions).{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em 1}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEs}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em 2}}
^{
\mathsf{Chg}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEs}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{name}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em 1}}
\right)
= 
\hspace*{2pt}
\mathtt{name}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em 2}}
\right)
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{T}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em fe}_{\mbox{\scriptsize\em 2}}
. 
\mathtt{name}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathsf{CHANGEME}
\hspace*{3pt}
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\vee 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{name}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em 1}}
\right)
= 
\\
\mathtt{abbrev}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em 2}}
\right)
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{T}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em fe}_{\mbox{\scriptsize\em 2}}
. 
\mathtt{abbrev}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{name}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em 2}}
\right)
\hspace*{3pt}
\\
\end{array}
\right\}
,
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{T}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em fe}_{\mbox{\scriptsize\em 2}}
. 
\mathtt{abbrev}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{nilS}
\hspace*{3pt}
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\vee 
\\
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{abbrev}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em 1}}
\right)
= 
\\
\mathtt{abbrev}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em 2}}
\right)
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{T}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em fe}_{\mbox{\scriptsize\em 2}}
. 
\mathtt{abbrev}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathsf{CHANGEME}
\hspace*{3pt}
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\wedge 
\\
\neg 
\hspace*{2pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{abbrev}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em 2}}
\right)
= 
\\
\mathtt{nilS}
\\
\end{array}
\\
\left\{
\left\{
\right\}
\right\}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\right)
\\
\implies 
\\
\mathtt{ident}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em 1}}
\right)
= 
\hspace*{2pt}
\mathtt{ident}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em 2}}
\right)
\left\{
\left\{
\right\}
\right\}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: frames\_definition\_FEs\_exist\label{rule_generated:frames_definition_FEs_exist} importance: 48\newline Within each Frame's definition for each referenced Frame Element we find a corresponding Frame Element (equal name or abbreviation) bound to this Frame.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em def}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{getFrameXMLDef}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}
\right)
\\
\end{array}
\right]
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em ref}}
^{
\mathsf{Chg}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{refFEs}
\left(
\mbox{\em frame}_{\mbox{\scriptsize\em def}}
\right)
\cup 
\\
\mathtt{concatMap}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{refFEs}
,
\\
\mathtt{examples}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}_{\mbox{\scriptsize\em def}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\\
\end{array}
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEs}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{name}
\left(
\mbox{\em fe}
\right)
= 
\hspace*{2pt}
\mbox{\em fe}_{\mbox{\scriptsize\em ref}}
\\
\left\{
\left\{
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em fe}_{\mbox{\scriptsize\em ref}}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{name}
\left(
\mbox{\em fe}
\right)
\hspace*{3pt}
\right\}
\right\}
\\
\end{array}
\\
\vee 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{abbrev}
\left(
\mbox{\em fe}
\right)
= 
\hspace*{2pt}
\mbox{\em fe}_{\mbox{\scriptsize\em ref}}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em fe}_{\mbox{\scriptsize\em ref}}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{abbrev}
\left(
\mbox{\em fe}
\right)
\hspace*{3pt}
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: frames\_fe\_definition\_FEs\_exist\label{rule_generated:frames_fe_definition_FEs_exist} importance: 48\newline Within the definition of a Frame Element belonging to a Frame F, for each referenced Frame Element we find a corresponding Frame Element (equal name or abbreviation) bound to the Frame F.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fes}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\left[
\mathtt{getFEs}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}
\right)
\right]
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mbox{\em fes}
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em def}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{getFEXMLDef}
\left(
\mathtt{fnDB}
,
\mbox{\em fe}
\right)
\\
\end{array}
\right]
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em ref}}
^{
\mathsf{Chg}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{refFEs}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em def}}
\right)
\cup 
\\
\mathtt{concatMap}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{refFEs}
,
\\
\mathtt{examples}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em def}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\\
\end{array}
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em for}_{\mbox{\scriptsize\em ref}}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mbox{\em fes}
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{name}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em for}_{\mbox{\scriptsize\em ref}}}
\right)
= 
\\
\mbox{\em fe}_{\mbox{\scriptsize\em ref}}
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em fe}_{\mbox{\scriptsize\em ref}}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{name}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em for}_{\mbox{\scriptsize\em ref}}}
\right)
\hspace*{3pt}
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\vee 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{abbrev}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em for}_{\mbox{\scriptsize\em ref}}}
\right)
= 
\\
\mbox{\em fe}_{\mbox{\scriptsize\em ref}}
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em fe}_{\mbox{\scriptsize\em ref}}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{abbrev}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em for}_{\mbox{\scriptsize\em ref}}}
\right)
\hspace*{3pt}
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: frames\_core\_FEs\_have\_example\_at\_all\label{rule_generated:frames_core_FEs_have_example_at_all} importance: 40\newline Each core (or core-unexpressed) FE of a (not non-lexical) Frame has examples (not necessarily marking this Frame Element).{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em st}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameSTs}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}
\right)
\hspace*{5pt}
\bullet 
\\
\neg 
\hspace*{2pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{name}
\left(
\mbox{\em st}
\right)
= 
\\
\mathsf{Non-Lexical Frame}
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em st}
. 
\mathtt{name}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathsf{Non-Lexical Frame}
\hspace*{3pt}
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\right)
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEs}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mbox{\em fe}
\right)
= 
\hspace*{2pt}
\mathtt{Core}
\\
\vee 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mbox{\em fe}
\right)
= 
\\
\mathtt{CoreUnexpressed}
\\
\end{array}
\\
\end{array}
\right)
\\
\implies 
\\
\neg 
\hspace*{2pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{null}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{examples}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{getFEXMLDef}
\left(
\mathtt{fnDB}
,
\mbox{\em fe}
\right)
\\
\end{array}
\right)
\\
\end{array}
\right)
\\
\\
\end{array}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\]


}

Rule: frames\_have\_example\_at\_all\label{rule_generated:frames_have_example_at_all} importance: 40\newline Each (not non-lexical) Frame has at least one example in the Frame definition.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em st}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameSTs}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}
\right)
\hspace*{5pt}
\bullet 
\\
\neg 
\hspace*{2pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{name}
\left(
\mbox{\em st}
\right)
= 
\\
\mathsf{Non-Lexical Frame}
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em st}
. 
\mathtt{name}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathsf{Non-Lexical Frame}
\hspace*{3pt}
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\right)
\\
\implies 
\\
\neg 
\hspace*{2pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{null}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{examples}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{getFrameXMLDef}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}
\right)
\\
\end{array}
\right)
\\
\end{array}
\right)
\\
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: frames\_core\_FEs\_accounted\_in\_frame\_definition\label{rule_generated:frames_core_FEs_accounted_in_frame_definition} importance: 35\newline Each core (and core-unexpressed) FE of a Frame is accounted for in the Frame's definition.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEs}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mbox{\em fe}
\right)
= 
\hspace*{2pt}
\mathtt{Core}
\\
\vee 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mbox{\em fe}
\right)
= 
\\
\mathtt{CoreUnexpressed}
\\
\end{array}
\\
\end{array}
\right)
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em def}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{getFrameXMLDef}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}
\\
\end{array}
\right)
\\
\end{array}
\right]
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em ref}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{refFEs}
\left(
\mbox{\em frame}_{\mbox{\scriptsize\em def}}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{name}
\left(
\mbox{\em fe}
\right)
= 
\hspace*{2pt}
\mbox{\em fe}_{\mbox{\scriptsize\em ref}}
\\
\vee 
\\
\mathtt{abbrev}
\left(
\mbox{\em fe}
\right)
= 
\hspace*{2pt}
\mbox{\em fe}_{\mbox{\scriptsize\em ref}}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: frames\_FE\_definition\_targets\_have\_same\_frame\label{rule_generated:frames_FE_definition_targets_have_same_frame} importance: 30\newline Each annotated target of each Frame Element example of a Frame actually evokes that Frame.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEs}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em def}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{getFEXMLDef}
\left(
\mathtt{fnDB}
,
\mbox{\em fe}
\right)
\\
\end{array}
\right]
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em targets}_{\mbox{\scriptsize\em ref}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{refTargets}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em def}}
\right)
\cup 
\\
\mathtt{concatMap}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{refTargets}
,
\\
\mathtt{examples}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em def}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\\
\end{array}
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em target}_{\mbox{\scriptsize\em ref}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{wordsS}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em targets}_{\mbox{\scriptsize\em ref}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em target}}
^{
\mathsf{Add}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getWordFrames}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em target}_{\mbox{\scriptsize\em ref}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}
= 
\hspace*{2pt}
\mbox{\em frame}_{\mbox{\scriptsize\em target}}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em frame}_{\mbox{\scriptsize\em target}}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mbox{\em frame}
\hspace*{3pt}
3
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: frames\_core\_FEs\_have\_example\_in\_fedef\label{rule_generated:frames_core_FEs_have_example_in_fedef} importance: 30\newline For each core (or core-unexpressed) FE of a (not non-lexical) Frame we find an example in the FE definition.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em st}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameSTs}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}
\right)
\hspace*{5pt}
\bullet 
\\
\neg 
\hspace*{2pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{name}
\left(
\mbox{\em st}
\right)
= 
\\
\mathsf{Non-Lexical Frame}
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em st}
. 
\mathtt{name}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathsf{Non-Lexical Frame}
\hspace*{3pt}
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\right)
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEs}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mbox{\em fe}
\right)
= 
\hspace*{2pt}
\mathtt{Core}
\\
\vee 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mbox{\em fe}
\right)
= 
\\
\mathtt{CoreUnexpressed}
\\
\end{array}
\\
\end{array}
\right)
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em ref}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{concatMap}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{refFEs}
,
\\
\mathtt{examples}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{getFEXMLDef}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em fe}
\\
\end{array}
\right)
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{name}
\left(
\mbox{\em fe}
\right)
= 
\hspace*{2pt}
\mbox{\em fe}_{\mbox{\scriptsize\em ref}}
\\
\vee 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{abbrev}
\left(
\mbox{\em fe}
\right)
= 
\\
\mbox{\em fe}_{\mbox{\scriptsize\em ref}}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\]


}

Rule: frames\_core\_FEs\_have\_example\_in\_framedef\label{rule_generated:frames_core_FEs_have_example_in_framedef} importance: 30\newline Each core (or core-unexpressed) FE of a (not non-lexical) Frame we find an example in the Frame definition.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em st}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameSTs}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}
\right)
\hspace*{5pt}
\bullet 
\\
\neg 
\hspace*{2pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{name}
\left(
\mbox{\em st}
\right)
= 
\\
\mathsf{Non-Lexical Frame}
\\
\end{array}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em st}
. 
\mathtt{name}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathsf{Non-Lexical Frame}
\hspace*{3pt}
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\right)
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEs}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mbox{\em fe}
\right)
= 
\hspace*{2pt}
\mathtt{Core}
\\
\vee 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mbox{\em fe}
\right)
= 
\\
\mathtt{CoreUnexpressed}
\\
\end{array}
\\
\end{array}
\right)
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em ref}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{concatMap}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{refFEs}
,
\\
\mathtt{examples}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{getFrameXMLDef}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}
\\
\end{array}
\right)
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{name}
\left(
\mbox{\em fe}
\right)
= 
\hspace*{2pt}
\mbox{\em fe}_{\mbox{\scriptsize\em ref}}
\\
\vee 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{abbrev}
\left(
\mbox{\em fe}
\right)
= 
\\
\mbox{\em fe}_{\mbox{\scriptsize\em ref}}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\]


}

Rule: frames\_definition\_targets\_have\_same\_frame\label{rule_generated:frames_definition_targets_have_same_frame} importance: 30\newline Each annotated target in a Frame example actually evokes that Frame.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em def}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{getFrameXMLDef}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}
\right)
\\
\end{array}
\right]
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em targets}_{\mbox{\scriptsize\em ref}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{refTargets}
\left(
\mbox{\em frame}_{\mbox{\scriptsize\em def}}
\right)
\cup 
\\
\mathtt{concatMap}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{refTargets}
,
\\
\mathtt{examples}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}_{\mbox{\scriptsize\em def}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\\
\end{array}
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em target}_{\mbox{\scriptsize\em ref}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{wordsS}
\left(
\mbox{\em targets}_{\mbox{\scriptsize\em ref}}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em target}}
^{
\mathsf{Add}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getWordFrames}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em target}_{\mbox{\scriptsize\em ref}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}
= 
\hspace*{2pt}
\mbox{\em frame}_{\mbox{\scriptsize\em target}}
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em frame}_{\mbox{\scriptsize\em target}}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mbox{\em frame}
\hspace*{3pt}
3
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: seealso\_target\_mentions\_source\label{rule_generated:seealso_target_mentions_source} importance: 30\newline If a Frame A points to B via Seealso then the definition of B should mention Frame A.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameRelationsByType}
\left(
\mathtt{fnDB}
,
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{See}_{\mbox{\scriptsize\em also}}
\\
\end{array}
\right]
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em src}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameByID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{source}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em trg}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameByID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{target}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{name}
\left(
\mbox{\em frame}_{\mbox{\scriptsize\em src}}
\right)
\in 
\\
\mathtt{map}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{trimS}
,
\\
\mathtt{wordsS}
\left(
\mathtt{getFrameDef}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}_{\mbox{\scriptsize\em trg}}
\right)
\right)
\\
\end{array}
\right)
\\
\end{array}
\\
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: frames\_core\_FEs\_definition\_exist\label{rule_generated:frames_core_FEs_definition_exist} importance: 25\newline Each core (or core-unexpressed) FE of a Frame has a definition, i.e., it is referenced in its own definition.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEs}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mbox{\em fe}
\right)
= 
\hspace*{2pt}
\mathtt{Core}
\\
\vee 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{feType}
\left(
\mbox{\em fe}
\right)
= 
\\
\mathtt{CoreUnexpressed}
\\
\end{array}
\\
\end{array}
\right)
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em ref}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{refFEs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{getFEXMLDef}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em fe}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{name}
\left(
\mbox{\em fe}
\right)
= 
\hspace*{2pt}
\mbox{\em fe}_{\mbox{\scriptsize\em ref}}
\\
\vee 
\\
\mathtt{abbrev}
\left(
\mbox{\em fe}
\right)
= 
\hspace*{2pt}
\mbox{\em fe}_{\mbox{\scriptsize\em ref}}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: docu\_docs\_parsable\label{rule_generated:docu_docs_parsable} importance: 20\newline Each document of the documentation is parsable.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em doc}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFNDocs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDocu}
,
\\
\mathtt{repHead}
\left(
\mathtt{fnDocu}
\right)
,
\\
\mathsf{trfn3.tex}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\neg 
\hspace*{2pt}
\mathtt{null}
\left(
\mathtt{dContent}
\left(
\mbox{\em doc}
\right)
\right)
\\
\end{array}
\]


}

Rule: docu\_ref\_fes\_exist\_in\_db\label{rule_generated:docu_ref_fes_exist_in_db} importance: 10\newline For each frame element referenced in the documentation we find a frame element in the database with the same name.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em doc}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFNDocs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDocu}
,
\\
\mathtt{repHead}
\left(
\mathtt{fnDocu}
\right)
,
\\
\mathsf{trfn3.tex}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em ref}_{\mbox{\scriptsize\em fe}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFNDocContents}
\left(
\mbox{\em doc}
,
\mathtt{refFEName}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFEs}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\mathtt{content}
\left(
\mbox{\em ref}_{\mbox{\scriptsize\em fe}}
\right)
= 
\hspace*{2pt}
\mathtt{name}
\left(
\mbox{\em fe}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: docu\_ref\_frames\_exist\_in\_db\label{rule_generated:docu_ref_frames_exist_in_db} importance: 10\newline For each frame referenced in the documentation we find a frame in the database with the same name.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em doc}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFNDocs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDocu}
,
\\
\mathtt{repHead}
\left(
\mathtt{fnDocu}
\right)
,
\\
\mathsf{trfn3.tex}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em ref}_{\mbox{\scriptsize\em frame}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFNDocContents}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em doc}
,
\\
\mathtt{refFrameName}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em frame}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\mathtt{content}
\left(
\mbox{\em ref}_{\mbox{\scriptsize\em frame}}
\right)
= 
\hspace*{2pt}
\mathtt{name}
\left(
\mbox{\em frame}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: docu\_ref\_LUs\_Lexemes\_exist\_in\_db\label{rule_generated:docu_ref_LUs_Lexemes_exist_in_db} importance: 5\newline For each LU or Lexeme marked as \ment{} in the documentation we find a similar LU or a similar Lexeme in the database. Comparison is not case sensitive, white spaces might be any character in the DB. Multi-word LUs Lexemes are taken into account. Words separated by any punctuation symbol are treated as extra LUs / Lexemes.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em doc}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFNDocs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDocu}
,
\\
\mathtt{repHead}
\left(
\mathtt{fnDocu}
\right)
,
\\
\mathsf{trfn3.tex}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em ref}_{\mbox{\scriptsize\em LU}_{\mbox{\scriptsize\em Lex}}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFNDocContents}
\left(
\mbox{\em doc}
,
\mathtt{refLU}_{\mbox{\scriptsize\em Lex}}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em phrase}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{splitPunctuation}
\left(
\mathtt{content}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em ref}_{\mbox{\scriptsize\em LU}_{\mbox{\scriptsize\em Lex}}}
\\
\end{array}
\right)
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\neg 
\hspace*{2pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{null}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{getSimilarLUs}
\left(
\mathtt{fnDB}
,
\mbox{\em phrase}
\right)
\\
\end{array}
\right)
\\
\\
\end{array}
\\
\vee 
\\
\neg 
\hspace*{2pt}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{null}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{getSimilarLexemes}
\left(
\mathtt{fnDB}
,
\mbox{\em phrase}
\right)
\\
\end{array}
\right)
\\
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: docu\_fenames\_annotated\label{rule_generated:docu_fenames_annotated} importance: 0\newline For each sentence we require that if the sentence is about frame elements then there is no not annotated word equal to a frame element name in the database (i.e. all frame element names are properly annotated).{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em doc}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFNDocs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDocu}
,
\\
\mathtt{repHead}
\left(
\mathtt{fnDocu}
\right)
,
\\
\mathsf{trfn3.tex}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em sentence}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getSentences}
\left(
\mbox{\em doc}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{isAboutFE}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{map}
\left(
\mathtt{content}
,
\mbox{\em sentence}
\right)
\\
\end{array}
\right)
\\
\\
\end{array}
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em context}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mbox{\em sentence}
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em word}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{map}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{trimS}
,
\\
\mathtt{wordsS}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{getText}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{content}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em context}
\\
\end{array}
\right)
\\
\end{array}
\right)
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{mightBeFEName}
\left(
\mbox{\em word}
\right)
\\
\implies 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{null}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{getFEByName}
\left(
\mathtt{fnDB}
,
\mbox{\em word}
\right)
\\
\end{array}
\right)
\\
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: docu\_framenames\_annotated\label{rule_generated:docu_framenames_annotated} importance: 0\newline For each sentence we require that if the sentence is about frames then there is no not annotated word equal to a frame name in the database (i.e. all frame names are properly annotated).{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em doc}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFNDocs}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDocu}
,
\\
\mathtt{repHead}
\left(
\mathtt{fnDocu}
\right)
,
\\
\mathsf{trfn3.tex}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em sentence}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getSentences}
\left(
\mbox{\em doc}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{isAboutFrame}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{map}
\left(
\mathtt{content}
,
\mbox{\em sentence}
\right)
\\
\end{array}
\right)
\\
\\
\end{array}
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em context}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mbox{\em sentence}
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em word}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{map}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{trimS}
,
\\
\mathtt{wordsS}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{getText}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{content}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em context}
\\
\end{array}
\right)
\\
\end{array}
\right)
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{mightBeFrameName}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em word}
\\
\end{array}
\right)
\\
\\
\end{array}
\\
\implies 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{null}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{getFrameByName}
\left(
\mathtt{fnDB}
,
\mbox{\em word}
\right)
\\
\end{array}
\right)
\\
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: each\_frame\_is\_connected\_via\_inheritance\label{rule_generated:each_frame_is_connected_via_inheritance} importance: 0\newline Each Frame is in the inheritance hierarchy.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}
^{
\mathsf{Del}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em rel}
^{
\mathsf{Add}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameRelationsByType}
\left(
\mathtt{fnDB}
,
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Inheritance}
\\
\end{array}
\right]
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{source}
\left(
\mbox{\em rel}
\right)
= 
\hspace*{2pt}
\mathtt{ident}
\left(
\mbox{\em frame}
\right)
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em rel}
. 
\mathtt{source}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{ident}
\left(
\mbox{\em frame}
\right)
\hspace*{3pt}
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\vee 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{target}
\left(
\mbox{\em rel}
\right)
= 
\hspace*{2pt}
\mathtt{ident}
\left(
\mbox{\em frame}
\right)
\\
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left\{
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{F}
: 
\hspace*{3pt}
\hspace*{3pt}
\mbox{\em rel}
. 
\mathtt{target}
\hspace*{3pt}
\rightsquigarrow 
\hspace*{3pt}
\mathtt{ident}
\left(
\mbox{\em frame}
\right)
\hspace*{3pt}
\\
\end{array}
\right\}
\\
\end{array}
\right\}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}

Rule: inheritance\_mapped\_FEs\_same\_name\label{rule_generated:inheritance_mapped_FEs_same_name} importance: 0\newline The Frame Elements that are mapped to each other as part of an inheritance relation should have the same names.
This is no really formal rule but good to know for AI applications.
Therefore, its priority is set to 0.{\small

\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{target}
,
\\
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Inheritance}
\\
\end{array}
\right]
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameByID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{source}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fechild-feparent}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFEMappings}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{name}
\left(
\mathtt{fst}
\left(
\mbox{\em fechild-feparent}
\right)
\right)
= 
\\
\mathtt{name}
\left(
\mathtt{snd}
\left(
\mbox{\em fechild-feparent}
\right)
\right)
\\
\end{array}
\\
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]


}