Common Syntax of the DFG-Schwerpunktprogramm Deduktion
Version 1.3

Reiner Hähnle
Fakultät für Informatik
Universität Karlsruhe
D-76128 Karlsruhe
reiner@ira.uka.de
Manfred Kerber
School of Computer Science
The University of Birmingham
Birmingham, B15 2TT, England
M.Kerber@cs.bham.ac.uk
Christoph Weidenbach
Max-Planck-Institut für Informatik
Im Stadtwald
66123 Saarbrücken
weidenb@mpi-sb.mpg.de

Zusammenfassung:

A common exchange format for logic problems to be used by members of the DFG-Schwerpunktprogramm Deduktion is introduced. It is thought to be a format that can easily be parsed such that it forms a compromise between the needs of the different groups. The language is partly more general than other popular exchange formats such as Otter or TPTP in allowing non-clausal and sorted formulae, several proof formats as well as user-defined operators. The latter feature makes it also useful for non-classical logics.