The postdoctoral research associate will carry out much of the engineering work associated with this proposal. In particular, we expect that he or she will actually design and implement the ``glue'' routines to connect existing mathematical software to the MathBus. We will hire postdoctoral research associates familiar with large-scale software development and who also are acquainted with the use of mathematical software and/or formal logic.