Comparing Approaches to the Exploration of the Domain of Residue Classes

A Meier, Martin Pollet, Volker Sorge

Research output: Contribution to journalArticle

15 Citations (Scopus)


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. (C) 2002 Elsevier Science Ltd. All rights reserved.
Original languageEnglish
Pages (from-to)287-306
Number of pages20
JournalJournal of Symbolic Computation
Issue number4
Publication statusPublished - 1 Oct 2002


Dive into the research topics of 'Comparing Approaches to the Exploration of the Domain of Residue Classes'. Together they form a unique fingerprint.

Cite this