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
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.
Uwe Brahm
1999-09-15