Examples

Next: Proofs Up: The Logical Parts Previous: The Logical Parts

Examples

We start with a complete description of Pelletier's [7] problem No. 57 that can be found in Figure 1. The syntax for the description part is explained in Section 6.

**Abbildung 1:** Pelletier's Problem No. 57
$\begin{figure}\begin{center} \tt \fbox{\begin{tabular}{l} begin\_problem(Pelleti... ...\ end\_of\_list.\\ \\ end\_problem.\\ \end{tabular}}\end{center}\end{figure}$

Our second example, Figure 2, uses the language features provided for the declaration of sorts.

**Abbildung 2:** Example with Sort Declarations
$\begin{figure}\begin{center} \tt \fbox{\begin{tabular}{l} begin\_problem(Sorts).... ... end\_of\_list. \\ \\ end\_problem.\\ \end{tabular}}\end{center}\end{figure}$

Uwe Brahm
1999-09-15