"a program which determines and outputs its term tree to any term of given signature"

The project was developed by the students Daniel Breest and Christoph Wagner. The major part of the work was completed under Linux (Kernel 2.0.30), with Motif 2.0.0. As target platform a HP workstation with HP-UX and Motif 1.2 was available. Starting point of the project was a C-practical training problem to prepare "a program which determines and outputs its term tree to any term of given signature."
For the correct representation apart from the actual term additionally still another signature is needed. This is divided into sorts and operators: the sorts are designators for quantities, which can contain constants (e.g. 1, 2 or 324) and variables (e.g. x, y or pax); Operators are defined as relation, whereby both the input sorts and the output sort are indicated. In the program thus, before a term can be input, the sorts and operators must be input. The program controls the correctness of the term, but also the correctness of the operators and sorts. The implementation runs thereby completely over string analyses. The implementation of an import/export interface was likewise important, over which on simplest way and operating system-independent way terms and signatures can be exchanged with other programs. Because of the latter no binary format, but a title format was thus selected. Reading the files in, the correctness of signatures and terms will be analyzed and compared to the data already in the data base available.
In order to get a small overview of the use of the program, follow these steps: As example the term "add(1,sk(vadd(a,b),vadd(c,d)))" should be used. In addition we define first a sort designator natZahl with the constant of 1. This occurs in the input field, which after click on the new Button beside the first list field appears. Write: natZahl(1)< Enter >. The definition appears in the list window of the sorts. Furthermore still the sort of the vectors is needed: vectSort(a, b, c, d)< Enter >. Thereby are determined the related variables and constants. Now the operators on the same way can be input. First the addition for natural numbers: After click on the new Button beside the second field appears those already well-known input box, which is completed around a list in the top. It serves for simply inserting defined sorts by doubleclicking. Write: add( and doubleclick on the sort natZahl. How you can see, additionally a comma is added, in order to be able to enter fast several sorts consecutively. After the input the operator is add(natZahl, natZahl, natZahl) in the list of the operators. The first two sorts are for the input sorts, which are naturally identical during the addition of natural numbers. The third sort determines the output sort of the operator; the sort thus, which can be understood as result of the operation. The same mirror-image moose again with with the dot product sk(vectSort, vectSort, natZahl) and the vektoraddition vadd(vectSort, vectSort, vectSort). Now finally the actual term can be input. Click on the new Button beside the third field. Now the long-known input window appears, in whose top now the operators are available for simply inserting. Now type the term in, which would have to be analyzed then by the program and found correct: add(1,sk(vadd(a,b),vadd(c,d))). Now mark the term in the list windows and click "Termbaum-Ausgabe". Thats all.

Screenshot Term

Screenshot Main-Application