Trustable Communication Between Mathematics Systems

Jacques Carette, William M. Farmer, and Jeremie Wajs

2004

Abstract

This paper presents a rigorous, unified framework for facilitating
communication between mathematics systems.  A mathematics system is
given one or more interfaces which offer deductive and computational
services to other mathematics systems.  To achieve communication
between systems, a client interface is linked to a server interface by
an asymmetric connection consisting of a pair of translations.
Answers to requests are trustable in the sense that they are correct
provided a small set of prescribed conditions are satisfied.  The
framework is robust with respect to interface extension and can
process requests for abstract services, where the server interface is
not fully specified.

Keywords: Mechanized mathematics, computer theorem proving, computer
algebra, intersystem communication, knowledge representation,
mathematical knowledge management.