Newer
Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
\section{ULO Predicates Used in Coq and Isabelle Exports}\label{sec:used}
Only a subset of the upper level ontology are actually taken
advantage of in the existing Coq and Isabelle exports. This
section lists which predicates are used and wich are not.
\subsection*{ULO Predicates used in the Isabelle Exports}
\begin{flushleft}
\texttt{check-time} \texttt{defines} \texttt{definition}
\texttt{derived} \texttt{experimental}
\texttt{external-size} \texttt{function}
\texttt{important} \texttt{inductive-on}
\texttt{instance-of} \texttt{justifies} \texttt{name}
\texttt{para} \texttt{paratype} \texttt{predicate}
\texttt{primitive} \texttt{section} \texttt{sourceref}
\texttt{specified-in} \texttt{specifies}
\texttt{statement} \texttt{theory} \texttt{type}
\texttt{unimportant} \texttt{universe} \texttt{uses}
\end{flushleft}
\subsection*{ULO predicates \emph{not} used in the Isabelle exports.}
\begin{flushleft}
\texttt{action-times} \texttt{aligned-with}
\texttt{alternative-for} \texttt{antonym}
\texttt{automatically-proved} \texttt{axiom}
\texttt{constructs} \texttt{contains}
\texttt{counter-example-for} \texttt{crossrefs}
\texttt{declaration} \texttt{deprecated} \texttt{docref}
\texttt{example} \texttt{example-for} \texttt{file}
\texttt{folder} \texttt{formalizes} \texttt{generated-by}
\texttt{hypernym} \texttt{hyponym}
\texttt{implementation-uses}
\texttt{implementation-uses-implementation-of}
\texttt{implementation-uses-interface-of} \texttt{inspired-by}
\texttt{inter-statement} \texttt{interface-uses}
\texttt{interface-uses-implementation-of}
\texttt{interface-uses-interface-of} \texttt{internal-size}
\texttt{last-checked-at} \texttt{library}
\texttt{library-group} \texttt{logical}
\texttt{mutual-block} \texttt{nyms}
\texttt{organizational} \texttt{phrase} \texttt{physical}
\texttt{proof} \texttt{proposition} \texttt{revision}
\texttt{rule} \texttt{same-as} \texttt{see-also}
\texttt{similar-to} \texttt{size-properties}
\texttt{superseded-by} \texttt{theorem} \texttt{typedec}
\texttt{uses-implementation} \texttt{uses-interface}
\end{flushleft}
\subsection*{ULO predicates used in the Coq exports.}\label{fig:used}
\begin{flushleft}
\texttt{axiom} \texttt{definition}
\texttt{derived} \texttt{example} \texttt{file}
\texttt{folder} \texttt{internal-size}
\texttt{library} \texttt{library-group}
\texttt{predicate} \texttt{primitive}
\texttt{proposition} \texttt{revision}
\texttt{statement} \texttt{theory} \texttt{type}
\texttt{uses}
\end{flushleft}
\subsection*{ULO predicates \emph{not} used in the Coq exports.}\label{fig:used}
\begin{flushleft}
\texttt{action-times} \texttt{aligned-with}
\texttt{alternative-for} \texttt{antonym}
\texttt{automatically-proved} \texttt{check-time}
\texttt{constructs} \texttt{contains}
\texttt{counter-example-for} \texttt{crossrefs}
\texttt{declaration} \texttt{defines}
\texttt{deprecated} \texttt{docref}
\texttt{example-for} \texttt{experimental}
\texttt{external-size} \texttt{formalizes}
\texttt{function} \texttt{generated-by}
\texttt{hypernym} \texttt{hyponym}
\texttt{implementation-uses}
\texttt{implementation-uses-implementation-of}
\texttt{implementation-uses-interface-of}
\texttt{important} \texttt{inductive-on}
\texttt{inspired-by} \texttt{instance-of}
\texttt{inter-statement} \texttt{interface-uses}
\texttt{interface-uses-implementation-of}
\texttt{interface-uses-interface-of}
\texttt{justifies} \texttt{last-checked-at}
\texttt{logical} \texttt{mutual-block}
\texttt{name} \texttt{nyms}
\texttt{organizational} \texttt{para}
\texttt{paratype} \texttt{phrase}
\texttt{physical} \texttt{proof} \texttt{rule}
\texttt{same-as} \texttt{section}
\texttt{see-also} \texttt{similar-to}
\texttt{size-properties} \texttt{sourceref}
\texttt{specified-in} \texttt{specifies}
\texttt{superseded-by} \texttt{theorem}
\texttt{typedec} \texttt{unimportant}
\texttt{universe} \texttt{uses-implementation}
\texttt{uses-interface}
\end{flushleft}