Distributed Mathematical Problem Solving

Proceedings of the Fourth Bar-Ilan Symposium on Foundations of Artificial Intelligence

Volume

Proceedings of the Fourth Bar-Ilan Symposium on Foundations of Artificial Intelligence

Contents

Coupling computer algebra systems and theorem provers enables to extend the capabilities they have when standing alone. We report on an ongoing research project whose long term goal is to provide an open environment for doing mathematics including reasoners and symbolic calculators. It is extensible by users which can construct complex systems by combination and insertion of existing packages. These systems may be based on different logics, formalisms, data structures, interfaces. A result of this work is illustrated by a prototype implementation of an interface between Isabelle and Maple.