MathWeb
System description: The MathWeb software bus for distributed mathematical reasoning. 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.
Keywords for this software
References in zbMATH (referenced in 13 articles , 1 standard article )
Showing results 1 to 13 of 13.
Sorted by year (- Llano, Maria Teresa; Ireland, Andrew; Pease, Alison: Discovery of invariants through automated theory formation (2014) ioport
- Carette, Jacques; Farmer, William M.; Sorge, Volker: A rational reconstruction of a system for experimental mathematics (2007)
- Allen, S.F.; Bickford, M.; Constable, R.L.; Eaton, R.; Kreitz, C.; Lorigo, L.; Moran, E.: Innovations in computational type theory using Nuprl (2006)
- Colton, Simon; Muggleton, Stephen: Mathematical applications of inductive logic programming (2006)
- Colton, Simon; Muggleton, Stephen: Mathematical applications of inductive logic programming (2006) ioport
- Siekmann, Jörg; Benzmüller, Christoph; Autexier, Serge: Computer supported mathematics with $\Omega$MEGA (2006)
- Colton, Simon: Automated conjecture making in number theory using HR, Otter and Maple (2005)
- Kamareddine, Fairouz; Maarek, Manuel; Wells, J.B.: Flexible encoding of mathematics on the computer (2004)
- Lorigo, Lori; Kleinberg, Jon; Eaton, Richard; Constable, Robert: A graph-based approach towards discerning inherent structures in a digital library of formal mathematics (2004)
- Lyaletski, Alexander; Paskevich, Andrey; Verchinine, Konstantin: Theorem proving and proof verification in the system SAD (2004)
- Zimmer, Jürgen; Melis, Erica: Constraint solving for proof planning (2004)
- Zimmer, Jürgen; Dennis, Louise A.: Inductive theorem proving and computer algebra in the MathWeb Software Bus (2002)
- Zimmer, Jürgen; Kohlhase, Michael: System description: The MathWeb software bus for distributed mathematical reasoning (2002)