Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants

DOI10.1006/jsco.2001.0455zbMath1074.68077OpenAlexW2079280457MaRDI QIDQ597106

Arjeh M. Cohen, Hendrik Pieter Barendregt

Publication date: 6 August 2004

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/jsco.2001.0455

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30)

Related Items

Formal and efficient primality proofs by use of computer algebra oracles, Automatic deduction in (dynamic) geometry: Loci computation, Dealing with algebraic expressions over a field in Coq using Maple, Retargeting OpenAxiom to Poly/ML: Towards an Integrated Proof Assistants and Computer Algebra System Framework

Uses Software

• Automath
• OMDoc

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Formal and efficient primality proofs by use of computer algebra oracles
• Some tapas of computer algebra
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• Autarkic computations in formal proofs
• Syntactical and semantical properties of simple type theory
• The Search for a Finite Projective Plane of Order 10
• Lifting standard bases in filtered structures
• The Impact of the Lambda Calculus in Logic and Computer Science
• My Numbers, My Friends
• Psi-calculi in Isabelle
• On the role of OpenMath in interactive mathematical documents