System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning
- 278 Downloads
Automated reasoning systems have reached a high degree of maturity in the last decade. Many reasoning tasks can be delegated to an automated theorem prover (ATP) by encoding them into its interface logic, simply calling the system and waiting for a proof, which will arrive in less than a second in most cases. Despite this seemingly ideal situation, ATPs are seldom actually used by people other than their own developers. The reasons for this seem to be that it is difficult for practitioners of other fields to find information about theorem prover software, to decide which system is best suited for the problem at hand, installing it, and coping with the often idiosyncratic concrete input syntax. Of course, not only potential outside users face these problems, so that, more often than not, existing reasoning procedures are re-implemented instead of re-used.
KeywordsSystem Description Computer Algebra System Reasoning System Client Application Proof Assistant
Unable to display preview. Download preview PDF.
- [AKR00]A. Armando, M. Kohlhase, and S. Ranise. Communication protocols for mathematical services based on KQML and OMRS. In Proc. of the Calculemus Symposium 2000), St. Andrews (Scotland), August 6–7, 2000.Google Scholar
- [Col00]S. Colton. Automated Theory Formation in Pure Mathematics. PhD thesis, University of Edinburgh, Edinburgh, Scotland, 2000.Google Scholar
- [XRP]XML Remote Procedure Call Specification. http://www.xmlrpc.com/.
- [Moz]The mozart programming system. http://www.mozart-oz.org.
- [FK99]A. Franke and M. Kohlhase. System description: MathWeb, an agent-based communication layer for distributed automated theorem proving. In H. Ganzinger, ed., Proc. CADE-16, LNAI 1632, pp. 217–221. Springer 1999.Google Scholar
- [Got00]H. Gottliebsen. Transcendental Functions and Continuity Checking in PVS. In Proc. of TPHOLs’00, LNCS 1869, pp. 197–214, Springer 2000.Google Scholar
- [Mel00]E. Melis. The ‘Interactive Textbook’ project. In D. McAllester, ed., Proc. of CADE WS “Deduction and Education;”, LNAI 1831. Springer Verlag, 2000.Google Scholar
- [ORS92]S. Owre, J. M. Rushby, and N. Shankar. PVS: A Prototype Verification System. In D. Kapur, ed.Proc. of CADE-11, LNCS 607, pp. 748–752. Springer 1992.Google Scholar
- [SB02]J. Siekmann, C. Benzmüller et al. Proof development with ωmega. In A. Voronkov, ed., Proc. of CADE-18, LNAI Springer 2002.Google Scholar
- [SSY94]G. Sutcliffe, C. Suttner, and T. Yemenis. The TPTP problem library. In A. Bundy, ed., Proc. of CADE-12, LNAI 814, pp. 252–266. Springer 1994.Google Scholar