Common syntax of the DFG-Schwerpunktprogramm "Deduktion"

A common exchange format for logic problems to be used by members
of the DFG-Schwerpunktprogramm ``Deduktion'' is introduced. It is
thought to be an internal format that can easily be parsed such that
it forms a compromise between the needs of the different groups.
It is not intended to be a high-level general logic language that
is easy to read or to write. The language is more general than other
popular exchange formats such as Otter or TPTP in allowing non-clausal and
sorted formulas as well as user-defined operators and quantifiers.
The latter feature makes it also useful for non-classical logics.