=ADD=
=reftype=
14
=number=
00-29
=url=
ftp://ftp.risc.uni-linz.ac.at/pub/techreports/2000/00-29.ps.gz
=year=
2000
=month=
10
=author=
Kutsia; Teimuraz + Nakagawa; Koji
=title=
An Interface between Theorema and External Automated Deduction Systems
=abstract=
The interface between Theorema and external automated deduction systems 
implements a link providing a user with a tool for using external
provers 
within Theorema session in the same way as "internal" Theorema provers. 
Currently, 11 external systems are supported and links to the others can 
be easily incorporated. Also, the TPTP (Thousands of Problems of Theorem 
Provers - problem library) problem convertor to Theorema format is
described. 
=keywords=
Bliksem, E equational prover, Eqp, Gandalf, Ivy, Mace, Otter, Scott,
Spass, Vampire, Waldmeister
=sponsor=
FWF project P1302