Computer algebra meets automated theorem proving: Integrating Maple and PVS

DOI10.1007/3-540-44755-5_4MaRDI QIDQ4790649zbMATH OpenFDO

Authors A. A. Adams, Martin Dunstan, Hanne Gottliebsen, Tom Kelsey, Sam Owre, Ursula Martin Webb

Publication date 4 February 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2152/21520027, https://zenodo.org/record/810873

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30)

Recommendations

• scientific article; zbMATH DE number 517013
• A Skeptic's approach to combining HOL and Maple
• scientific article; zbMATH DE number 1254246
• Integrating computer algebra into proof planning
• Integrating systems around the user: combining Isabelle, Maple, and QEPCAD in the prover's palette

Cited in

(28)

• A Skeptic's approach to combining HOL and Maple
• Integrating computer algebra into proof planning
• PVS
• The formalization of discrete Fourier transform in HOL
• Verified interactive computation of definite integrals
• Modelling algebraic structures and morphisms in ACL2
• Hidden verification for computational mathematics
• Dealing with algebraic expressions over a field in Coq using Maple
• A bi-directional extensible interface between Lean and Mathematica
• Interactions between PVS and Maple in symbolic analysis of control systems
• Enabling symbolic and numerical computations in HOL Light
• A Brief Overview of PVS
• Specification and integration of theorem provers and computer algebra systems
• scientific article; zbMATH DE number 1254246 (Why is no real title available?)
• scientific article; zbMATH DE number 517013 (Why is no real title available?)
• Applications of real number theorem proving in PVS
• scientific article; zbMATH DE number 1389645 (Why is no real title available?)
• scientific article; zbMATH DE number 1389647 (Why is no real title available?)
• Proof verification and proof discovery for relativity
• Integrating systems around the user: combining Isabelle, Maple, and QEPCAD in the prover's palette
• Retargeting OpenAxiom to Poly/ML: towards an integrated proof assistants and computer algebra system framework
• Proof assistant decision procedures for formalizing origami
• Certified Computer Algebra on Top of an Interactive Theorem Prover
• Combining Isabelle and QEPCAD-B in the Prover’s Palette
• Interfacing external CA systems for Gröbner bases computation in Mizar proof checking
• Analytica -- an experiment in combining theorem proving and symbolic computation
• An interpreter for quantum circuits
• Providing a formal linkage between MDG and HOL

Describes a project that uses

Uses Software

• AXIOM
• Maple
• Theorema
• OMRS
• REDLOG
• PROSPER
• Isabelle
• Isar

This page was built for publication: Computer algebra meets automated theorem proving: Integrating Maple and PVS

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4790649)