ACM Portal
  Subscribe (Full Service)    Register (Limited Service, Free)    Login
  Search:   The ACM Digital Library   The Guide
  
ACM Home Page
Please provide us with feedback. Feedback
Theorems and algorithms: an interface between Isabelle and Maple
Full text PdfPdf (844 KB)
Source International Conference on Symbolic and Algebraic Computation archive
Proceedings of the 1995 international symposium on Symbolic and algebraic computation table of contents
Montreal, Quebec, Canada
Pages: 150 - 157  
Year of Publication: 1995
ISBN:0-89791-699-9
Authors
Clemens Ballarin  Universität Karlsruhe, Institut für Algorithmen und Kognitive Systeme, Am Fasanengarten 5. 76131 Karlsruhe, Germany
Karsten Homann  Universität Karlsruhe, Institut für Algorithmen und Kognitive Systeme, Am Fasanengarten 5. 76131 Karlsruhe, Germany
Jacques Calmet  Universität Karlsruhe, Institut für Algorithmen und Kognitive Systeme, Am Fasanengarten 5. 76131 Karlsruhe, Germany
Sponsors
SIGSAM: ACM Special Interest Group on Symbolic and Algebraic Manipulation
SIGNUM: ACM Special Interest Group on Numerical Mathematics
Publisher
ACM  New York, NY, USA
Bibliometrics
Downloads (6 Weeks): 2,   Downloads (12 Months): 9,   Citation Count: 9
Additional Information:

references   cited by   index terms   collaborative colleagues  

Tools and Actions: Request Permissions Request Permissions    Review this Article  
DOI Bookmark: Use this link to bookmark this Article: http://doi.acm.org/10.1145/220346.220366
What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

 
BALLARIN 94
C. BALLARIN Algorithmische Schritte in formalen Beweisen - Entwurf und Implementierung der Anbindung eines Computeralgebrasystems an einen Theorembeweiser. Diplomaxbeit, Universit~it Karlsruhe, 1994.
 
BüNDGEN 94
Reinhard Bündgen, Combining Computer Algebra and Rule Based Reasoning, Selected Papers from the Second International Conference on Integrating Symbolic Mathematical Computation and Artificial Intelligence, p.209-223, August 03-05, 1994
 
CALMET & CAMPBELL 94
Jacques Calmet , John A. Campbell, Artificial Intelligence and Symbolic Mathematical Computation, Proceedings of the International Conference on Artificial Intelligence and Symbolic Mathematical Computation, p.1-19, August 03-06, 1992
 
CALMET & HOMANN 95
J. CALMET, K. I--IOMANN Distributed Mathematical Problem Solving. In Proceedings of 4th Bar-Ilan Symposium on Foundations of Artificial Intelligence (BISFAI'95), 1995, to appear.
 
CHAR et al. 92
B.W. CHAR, K.O. GEDDES, G.H. GON- NET, B.L. LEONG, M.B. MONAGAN, S.M. WATT Maple V Language Reference Manual, Springer-Verlag, 1992.
 
CLARKE & ZHAO 94
Edmund M. Clarke , Xudong Zhao, Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan, Proceedings of the 12th International Conference on Automated Deduction, p.758-763, June 26-July 01, 1994
 
McCUNE 94
W.W. MCCUNE OTTER 3.0 Reference Manual and Guide, Technical Report ANL-94/6, Argonne National Labaratory, 1994.
 
GIUNCHIGLIA et al. 94
F. GIUNCHIGLIA, P. PECCHIARI, C. TALCOTT Reasoning Theories - Towards an Architecture for Open Mechanized Reasoning Systems, 1994, to appear.
 
HARRISON & THÉRY 93
John Harrison , Laurent Théry, Extending the HOL Theorem Prover with a Computer Algebra System to Reason about the Reals, Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and its Applications, p.174-184, August 11-13, 1993
 
HOMANN & CALMET 94
Karsten Homann , Jacques Calmet, Combining Theorem Proving and Symbolic Mathematical Computing, Selected Papers from the Second International Conference on Integrating Symbolic Mathematical Computation and Artificial Intelligence, p.18-29, August 03-05, 1994
 
JACKSON 94
Paul Jackson, Exploring Abstract Algebra in Constructive Type Theory, Proceedings of the 12th International Conference on Automated Deduction, p.590-604, June 26-July 01, 1994
KAJLER 92
Norbert Kajler, CAS/PI: a portable and extensible interface for computer algebra systems, Papers from the international symposium on Symbolic and algebraic computation, p.376-386, July 27-29, 1992, Berkeley, California, United States  [doi>10.1145/143242.143359]
 
MILNER 85
R. Milner, The use of machines to assist in rigorous proof, Proc. of a discussion meeting of the Royal Society of London on Mathematical logic and programming languages, p.77-88, June 1985, London, United Kingdom
 
MILNER & TOFTE 91
Robin Milner , Mads Tofte, Commentary on standard ML, MIT Press, Cambridge, MA, 1991
 
PAULSON 83
L.C. PAULSON A Higher-Order Implementation of Rewriting. In Science of Computer Programming 3, pp. 119-149, North Holland, 1983.
 
PAULSON 94
L.C. PAULSON Isabelle A Generic Theorem Prover, Lecture Notes in Computer Science 828, Springer-Verlag, 1994.
 
UEBERBERG 94
Johannes Ueberberg, Interactive Theorem Proving and Computer Algebra, Selected Papers from the Second International Conference on Integrating Symbolic Mathematical Computation and Artificial Intelligence, p.1-9, August 03-05, 1994
 
WOLFRAM 91
Stephen Wolfram, Mathematica: a system for doing mathematics by computer (2nd ed.), Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1991

CITED BY  9
O. Caprotti , A. M. Cohen, On the role of OpenMath in interactive mathematical documents, Journal of Symbolic Computation, v.32 n.4, p.351-364, October 2001
Alessandro Armando , Alessandro Coglio , Fausto Giunchiglia , Silvio Ranise, The control layer in open mechanized reasoning systems: annotations and tactics, Journal of Symbolic Computation, v.32 n.4, p.305-332, October 2001
Micheal Kohlhase , Andreas Franke, MBase: representing knowledge and context for the intergration of mathematical software systems, Journal of Symbolic Computation, v.32 n.4, p.365-402, October 2001
A. A. Adams , H. Gottliebsen , S. A. Linton , U. Martin, Automated theorem proving in support of computer algebra: symbolic definite integration as a case study, Proceedings of the 1999 international symposium on Symbolic and algebraic computation, p.253-260, July 28-31, 1999, Vancouver, British Columbia, Canada
F. Giunchiglia , P. Pecchiari , C. Talcott, Reasoning Theories, Journal of Automated Reasoning, v.26 n.3, p.291-331, April 2001
J. Harrison , L. Théry, A Skeptic’s Approach to Combining HOL and Maple, Journal of Automated Reasoning, v.21 n.3, p.279-294, December 1998
Andrej Bauer , Edmund Clarke , Xudong Zhao, Analytica – An Experiment in Combining Theorem Proving and Symbolic Computation, Journal of Automated Reasoning, v.21 n.3, p.295-325, December 1998
Manfred Kerber , Michael Kohlhase , Volker Sorge, Integrating Computer Algebra into Proof Planning, Journal of Automated Reasoning, v.21 n.3, p.327-355, December 1998
Virgile Prevosto , Damien Doligez, Algorithms and Proofs Inheritance in the FOC Language, Journal of Automated Reasoning, v.29 n.3-4, p.337-363, 2002

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.3 Languages and Systems
          Subjects: Special-purpose algebraic systems

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

  G. Mathematics of Computing
  G.4 MATHEMATICAL SOFTWARE
      Subjects: Algorithm design and analysis

  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.3 Languages and Systems

          Nouns: Maple


General Terms:
Algorithms, Languages, Theory, Verification

Collaborative Colleagues:
Clemens Ballarin: colleagues
Karsten Homann: colleagues
Jacques Calmet: colleagues

The ACM Portal is published by the Association for Computing Machinery. Copyright © 2009 ACM, Inc.
Terms of Usage   Privacy Policy   Code of Ethics   Contact Us

Useful downloads: Adobe Acrobat    QuickTime    Windows Media Player    Real Player