next up previous
Next: Introduction

Common Syntax of the DFG-Schwerpunktprogramm Deduktion
Version 1.3

Reiner Hähnle
Fakultät für Informatik
Universität Karlsruhe
D-76128 Karlsruhe
Manfred Kerber
School of Computer Science
The University of Birmingham
Birmingham, B15 2TT, England
Christoph Weidenbach
Max-Planck-Institut für Informatik
Im Stadtwald
66123 Saarbrücken


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.


Uwe Brahm