Geoff Sutcliffe and Juergen Zimmer and Stephan Schulz:
Communication Formalisms for Automated Theorem Proving Tools

Abstract

This paper describes two communication formalisms for Automated
Theorem Proving (ATP) tools.  First, a problem and solution language
has been designed.  The language will be used for writing problems to
be input to ATP systems, and for writing solutions output by ATP
systems.  Second, a hierarchy of result statuses, which adequately
express the range of results output by ATP systems, has been
established.  These formalisms will support application and research
in ATP, and will facilitate direct communication between ATP tools
when they are used as embedded components in larger systems.