blob: c4790bb1bf38c5940ba7307a07d55c0c8036a8a6 (
plain)
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
|
\begin{abbreviation}\label{empty}
$x$ is empty iff there exists no $y$ such that $y\in x$.
\end{abbreviation}
\begin{proposition}\label{dummy_abbr_test_adj}
If $x$ is empty, then $x$ is empty.
\end{proposition}
% Dummy abbreviation to test noun abbreviations.
\begin{abbreviation}\label{function}
$x$ is a function iff $x = x$.
\end{abbreviation}
\begin{proposition}\label{dummy_abbr_test_noun}
$x$ is a function.
\end{proposition}
% Dummy abbreviation to test verb abbreviations.
\begin{abbreviation}\label{converges}
$x$ converges to $y$ iff $x = y$.
\end{abbreviation}
\begin{proposition}\label{dummy_abbr_test_verb}
If $x$ converges to $y$, then $x = y$.
\end{proposition}
% Test of built-in \notin abbreviation. The two variants should produce the same TPTP atoms.
\begin{proposition}\label{abbr_test_notin}
If $x\notin y$, then $x\not\in y$.
\end{proposition}
% Test of built-in "element of" abbreviation. The two variants should produce the same TPTP atoms.
\begin{proposition}\label{abbr_test_elementof_is_in}
If $x$ is an element of $y$, then $x\in y$.
\end{proposition}
% Test of built-in "equals" abbreviation. The two variants should produce the same TPTP atoms.
\begin{proposition}\label{abbr_test_equals_is_eq}
If $x$ equals $y$, then $x = y$.
\end{proposition}
|
