Comparing Approaches to the Exploration of the Domain of Residue Classes

We report on a case study on combining proof planning with computer algebra systems. We construct proofs for basic algebraic properties of residue classes as well as for isomorphisms between residue classes using different proof techniques, which are implemented as strategies in a multi-strategy pro...

Full description

Saved in:
Bibliographic Details
Published in:Journal of symbolic computation 2002-10, Vol.34 (4), p.287-306
Main Authors: Meier, Andreas, Pollet, Martin, Sorge, Volker
Format: Article
Language:English
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We report on a case study on combining proof planning with computer algebra systems. We construct proofs for basic algebraic properties of residue classes as well as for isomorphisms between residue classes using different proof techniques, which are implemented as strategies in a multi-strategy proof planner. The search space of the proof planner can be drastically reduced by employing computations of two computer algebra systems during the planning process. To test the effectiveness of our approach we carried out a large number of experiments and also compared it with some alternative approaches. In particular, we experimented with substituting computer algebra by model generation and by proving theorems with a first-order equational theorem prover instead of a proof planner.
ISSN:0747-7171
1095-855X
DOI:10.1006/jsco.2002.0550