article · 1997
A Sceptic's Approach to Combining HOL and Maple
J. Harrison, L. Théry, Inria Sophia Antipolis
Cited by 0Abstract and details only
Abstract
. We contrast theorem provers and computer algebra systems, pointing out the advantages and disadvantages of each, and suggest a simple way to achieve a synthesis of some of the best features of both. Our method is based on the systematic separation of search for a solution and checking the solution, using a physical connection between systems. We describe the separation of proof search and checking in some detail, relating it to proof planning and to the complexity class NP, and discuss different ways of exploiting a physical link between systems. Finally, the method is illustrated by some concrete examples of computer algebra results proved formally in the HOL theorem prover with the aid of Maple: the evaluation of trigonometric integrals. Key words: Proof checking, automated theorem proving, computer algebra, complexity theory JEL codes: ? 1. Theorem provers vs. computer algebra systems Computer algebra systems (CASs) seem superficially similar to computer theorem provers: both a...
Cite this paper
Harrison, J., Théry, L., & Antipolis, I. S. (1997). A Sceptic's Approach to Combining HOL and Maple.
Harrison, J., et al. “A Sceptic's Approach to Combining HOL and Maple.” 1997.
Harrison, J., L. Théry, and Inria Sophia Antipolis. 1997. “A Sceptic's Approach to Combining HOL and Maple.”
Harrison, J., Théry, L. and Antipolis, I.S. (1997) ‘A Sceptic's Approach to Combining HOL and Maple’.
@article{harrison1997sceptic,
title = {{A Sceptic's Approach to Combining HOL and Maple}},
author = {Harrison, J. and Théry, L. and Antipolis, Inria Sophia},
year = {1997}
}Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.