Back to Search
Start Over
Combining Automated Theorem Provers with Symbolic Algebraic Systems: Position Paper
- Publication Year :
- 1999
- Publisher :
- United States: NASA Center for Aerospace Information (CASI), 1999.
-
Abstract
- In contrast to pure mathematical applications where automated theorem provers (ATPs) are quite capable, proof tasks arising form real-world applications from the area of Software Engineering show quite different characteristics: they usually do not only contain much arithmetic (albeit often quite simple one), but they also often contain reasoning about specific structures (e.g. graphics, sets). Thus, an ATP must be capable of performing reasoning together with a fair amount of simplification, calculation and solving. Therefore, powerful simplifiers and other (symbolic and semi-symbolic) algorithms seem to be ideally suited to augment ATPs. In the following we shortly describe two major points of interest in combining SASs (symbolic algebraic systems) with top-down automated theorem provers (here: SETHEO [Let92, GLMS94]).
- Subjects :
- Numerical Analysis
Subjects
Details
- Language :
- English
- Database :
- NASA Technical Reports
- Publication Type :
- Report
- Accession number :
- edsnas.20000109821
- Document Type :
- Report